Definition df-rex 2528

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 2523	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1397	. . . . 5 class 𝑥
6	5, 3	wcel 2205	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1541	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 105	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  2532  rexnalim  2533  dfrex2dc  2535  rexbida  2539  rexbidv2  2547  rexbid2  2549  rexbii2  2555  r2exf  2562  risset  2572  nfrexdxy  2578  nfrexdya  2580  nfre1  2587  rexex  2590  rspe  2593  rsp2e  2595  rexim  2638  reximi2  2640  reximdv2  2643  r19.23t  2652  r19.41  2700  r19.43  2703  reean  2714  rexeqf  2740  reu5  2764  rmo5  2767  cbvrexfw  2770  cbvrexf  2772  cbvrexvw  2785  cbvrexdva2  2788  rexv  2834  2gencl  2849  3gencl  2850  rspce  2918  rspcimedv  2925  ceqsrexv  2950  rexab  2982  rexab2  2986  rexrab2  2987  morex  3004  reu2  3008  reu6  3009  reu3  3010  2reuswapdc  3024  2rmorex  3026  cbvrexcsf  3205  ssrexf  3304  rexun  3403  reuss2  3505  reuun2  3508  reupick  3509  reupick3  3510  reximdva0m  3528  rabn0r  3539  rabn0m  3540  r19.2m  3600  r19.2mOLD  3601  r19.9rmv  3605  rexm  3613  rexsns  3733  exsnrex  3736  dfuni2  3921  eluni2  3923  elunirab  3932  iuncom4  4003  iunxiun  4078  intexrabim  4270  bnd2  4291  rexxfrd  4589  elxp2  4772  opeliunxp  4810  xpiundi  4813  xpiundir  4814  rexiunxp  4902  ssrelrn  4952  dmuni  4971  rnmpt  5010  elrnmpt1  5013  elres  5079  dfima2  5108  dfima3  5109  elima2  5112  dfco2a  5268  imaco  5273  imadiflem  5440  imadif  5441  imainlem  5442  imain  5443  funimaexglem  5444  fvelrnb  5729  rexrnmpt  5825  dffo4  5830  dffo5  5831  abrexco  5938  opabex3d  6323  opabex3  6324  abexssex  6327  abexex  6328  ecexr  6785  mapsnd  6936  mapsn  6938  mapsnend  7065  mapsnen  7066  fimax2gtri  7172  ctssdccl  7415  ltexnqq  7739  subhalfnqq  7745  ltbtwnnq  7747  nqnq0  7772  prnmaxl  7819  prnminu  7820  prarloc  7834  genpdflem  7838  genpassl  7855  genpassu  7856  nqprm  7873  nqprl  7882  nqpru  7883  ltsopr  7927  ltexprlemm  7931  ltexprlemloc  7938  suplocexprlemrl  8048  suplocexprlemloc  8052  axprecex  8211  axpre-ltirr  8213  sup3exmid  9248  2rexuz  9932  ioom  10644  nnwosdc  12760  4sqlemafi  13118  inffinp1  13264  omctfn  13278  nninfdclemp1  13285  ptex  13561  fngsum  13651  igsumvalx  13652  isbasis2g  15036  tgval2  15042  ntreq0  15123  bdcuni  16772  bj-axun2  16811