Definition df-rex 2450

Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
df-rex	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

Detailed syntax breakdown of Definition df-rex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wrex 2445	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1342	. . . . 5 class 𝑥
6	5, 3	wcel 2136	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1480	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 104	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  2454  rexnalim  2455  dfrex2dc  2457  rexbida  2461  rexbidv2  2469  rexbid2  2471  rexbii2  2477  r2exf  2484  risset  2494  nfrexdxy  2500  nfrexdya  2502  nfre1  2509  rexex  2512  rspe  2515  rsp2e  2517  rexim  2560  reximi2  2562  reximdv2  2565  r19.23t  2573  r19.41  2621  r19.43  2624  reean  2634  rexeqf  2658  reu5  2678  rmo5  2681  cbvrexfw  2684  cbvrexf  2686  cbvrexvw  2697  cbvrexdva2  2700  rexv  2744  2gencl  2759  3gencl  2760  rspce  2825  rspcimedv  2832  ceqsrexv  2856  rexab  2888  rexab2  2892  rexrab2  2893  morex  2910  reu2  2914  reu6  2915  reu3  2916  2reuswapdc  2930  2rmorex  2932  cbvrexcsf  3108  ssrexf  3204  rexun  3302  reuss2  3402  reuun2  3405  reupick  3406  reupick3  3407  reximdva0m  3424  rabn0r  3435  rabn0m  3436  r19.2m  3495  r19.2mOLD  3496  r19.9rmv  3500  rexm  3508  rexsns  3615  exsnrex  3618  dfuni2  3791  eluni2  3793  elunirab  3802  iuncom4  3873  iunxiun  3947  intexrabim  4132  bnd2  4152  rexxfrd  4441  elxp2  4622  opeliunxp  4659  xpiundi  4662  xpiundir  4663  rexiunxp  4746  dmuni  4814  rnmpt  4852  elrnmpt1  4855  elres  4920  dfima2  4948  dfima3  4949  elima2  4952  dfco2a  5104  imaco  5109  imadiflem  5267  imadif  5268  imainlem  5269  imain  5270  funimaexglem  5271  fvelrnb  5534  rexrnmpt  5628  dffo4  5633  dffo5  5634  abrexco  5727  opabex3d  6089  opabex3  6090  abexssex  6093  abexex  6094  ecexr  6506  mapsn  6656  mapsnen  6777  fimax2gtri  6867  ctssdccl  7076  ltexnqq  7349  subhalfnqq  7355  ltbtwnnq  7357  nqnq0  7382  prnmaxl  7429  prnminu  7430  prarloc  7444  genpdflem  7448  genpassl  7465  genpassu  7466  nqprm  7483  nqprl  7492  nqpru  7493  ltsopr  7537  ltexprlemm  7541  ltexprlemloc  7548  suplocexprlemrl  7658  suplocexprlemloc  7662  axprecex  7821  axpre-ltirr  7823  sup3exmid  8852  2rexuz  9520  ioom  10196  nnwosdc  11972  inffinp1  12362  omctfn  12376  nninfdclemp1  12383  isbasis2g  12683  tgval2  12691  ntreq0  12772  bdcuni  13758  bj-axun2  13797