Definition df-rex 2517

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 2512	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1397	. . . . 5 class 𝑥
6	5, 3	wcel 2202	. . . 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  2521  rexnalim  2522  dfrex2dc  2524  rexbida  2528  rexbidv2  2536  rexbid2  2538  rexbii2  2544  r2exf  2551  risset  2561  nfrexdxy  2567  nfrexdya  2569  nfre1  2576  rexex  2579  rspe  2582  rsp2e  2584  rexim  2627  reximi2  2629  reximdv2  2632  r19.23t  2641  r19.41  2689  r19.43  2692  reean  2703  rexeqf  2728  reu5  2752  rmo5  2755  cbvrexfw  2758  cbvrexf  2760  cbvrexvw  2773  cbvrexdva2  2776  rexv  2822  2gencl  2837  3gencl  2838  rspce  2906  rspcimedv  2913  ceqsrexv  2937  rexab  2969  rexab2  2973  rexrab2  2974  morex  2991  reu2  2995  reu6  2996  reu3  2997  2reuswapdc  3011  2rmorex  3013  cbvrexcsf  3192  ssrexf  3290  rexun  3389  reuss2  3489  reuun2  3492  reupick  3493  reupick3  3494  reximdva0m  3512  rabn0r  3523  rabn0m  3524  r19.2m  3583  r19.2mOLD  3584  r19.9rmv  3588  rexm  3596  rexsns  3712  exsnrex  3715  dfuni2  3900  eluni2  3902  elunirab  3911  iuncom4  3982  iunxiun  4057  intexrabim  4248  bnd2  4269  rexxfrd  4566  elxp2  4749  opeliunxp  4787  xpiundi  4790  xpiundir  4791  rexiunxp  4878  ssrelrn  4928  dmuni  4947  rnmpt  4986  elrnmpt1  4989  elres  5055  dfima2  5084  dfima3  5085  elima2  5088  dfco2a  5244  imaco  5249  imadiflem  5416  imadif  5417  imainlem  5418  imain  5419  funimaexglem  5420  fvelrnb  5702  rexrnmpt  5798  dffo4  5803  dffo5  5804  abrexco  5910  opabex3d  6292  opabex3  6293  abexssex  6296  abexex  6297  ecexr  6750  mapsn  6902  mapsnen  7029  fimax2gtri  7134  ctssdccl  7370  ltexnqq  7688  subhalfnqq  7694  ltbtwnnq  7696  nqnq0  7721  prnmaxl  7768  prnminu  7769  prarloc  7783  genpdflem  7787  genpassl  7804  genpassu  7805  nqprm  7822  nqprl  7831  nqpru  7832  ltsopr  7876  ltexprlemm  7880  ltexprlemloc  7887  suplocexprlemrl  7997  suplocexprlemloc  8001  axprecex  8160  axpre-ltirr  8162  sup3exmid  9196  2rexuz  9877  ioom  10583  nnwosdc  12690  4sqlemafi  13048  inffinp1  13130  omctfn  13144  nninfdclemp1  13151  ptex  13427  fngsum  13551  igsumvalx  13552  isbasis2g  14856  tgval2  14862  ntreq0  14943  bdcuni  16592  bj-axun2  16631