Definition df-rex 1206

Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22.

Assertion

Ref	Expression
df-rex	⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))

Detailed syntax breakdown of Definition df-rex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	wrex 1202	. 2 wff ∃x ∈ A φ
5	2	cv 1089	. . . . 5 class x
6	5, 3	wcel 1092	. . . 4 wff x ∈ A
7	6, 1	wa 196	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	wex 678	. 2 wff ∃x(x ∈ A ∧ φ)
9	4, 8	wb 127	1 wff (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))

This definition is referenced by:  ralnex 1209  rexnal 1210  birexda 1214  birexdv2 1222  birex2 1227  risset 1235  hbrex 1238  hbre1 1239  r2ex 1241  rexex 1242  ra4e 1244  r19.22 1272  r19.22i2 1274  r19.22dv2 1277  r19.23v 1282  r19.23ai 1283  r19.23ad 1285  r19.23adv 1286  r19.29 1295  r19.41v 1302  r19.43 1304  reeanv 1316  rexeqf 1322  cbvrex 1332  reurex 1337  reu2 1338  reu5 1339  2reuswap 1341  rexv 1358  rcla4ev 1403  ceqsrexv 1413  reuss 1577  reupick 1578  rabn0 1716  rab0 1718  r19.2z 1766  dfuni2 1921  eluni2 1923  intexrab 1988  iunconst 2000  dfiun2 2014  dfiin2 2015  iunss 2017  ssiun 2018  iinss 2025  iunn0 2029  iunxsn 2034  iunxun 2035  iununi 2037  onminex 2275  nnsuc 2389  elxp2 2443  cbvop 2473  dmuni 2538  dfima2 2604  dfima3 2605  elima2 2607  rnuni 2646  imaiun 2650  zfrep6 2744  fv2 2828  fniunfv 2860  fvelrn 2883  abrexexlem1 2910  isomin 2937  iinon 2948  rdglim2 2987  elqs 3227  qsex 3231  snec 3232  mapsn 3269  mapsnen 3334  pssnn 3428  ssnn 3429  unblem2 3432  unfilem1 3438  zfregcl 3446  inf4 3473  zfinf 3474  r1pwcl 3530  scott0 3542  cp 3547  bnd2 3549  aceq1 3552  aceq5lem2 3559  aceq5lem3 3560  aceq6b 3565  ac6lem 3575  kmlem3 3582  kmlem6 3585  kmlem13 3592  kmlem14 3593  zornlem4 3606  zornlem6 3608  zornlem7 3609  cfub 3703  ltexpi 3823  prnmax 3893  genpcl 3905  1pr 3911  ltexprlem5 3940  reclem2pr 3951  suplem1pr 3955  axnegex 4078  axrecex 4079  axrnegex 4080  axrrecex 4081  axsup 4088  renegcl 4171  redivcl 4274  sup2 4510  nnunb 4520  creur 4532  creui 4533  nnwof 4609  nnwos 4610  replimt 4798  infxpidmlem9 4941  infxpidmlem10 4942  chsscm 5147  chcmh 5148  shless 5348  shne0 5372

metamath.org