Definition df-rex 2534

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

This definition is referenced by:  ralnex  2538  rexnalim  2539  dfrex2dc  2541  rexbida  2545  rexbidv2  2553  rexbid2  2555  rexbii2  2561  r2exf  2568  risset  2578  nfrexdxy  2584  nfrexdya  2586  nfre1  2593  rexex  2596  rspe  2599  rsp2e  2601  rexim  2644  reximi2  2646  reximdv2  2649  r19.23t  2658  r19.41  2706  r19.43  2709  reean  2720  rexeqf  2746  reu5  2770  rmo5  2773  cbvrexfw  2776  cbvrexf  2778  cbvrexvw  2791  cbvrexdva2  2794  rexv  2840  2gencl  2855  3gencl  2856  rspce  2924  rspcimedv  2931  ceqsrexv  2956  rexab  2988  rexab2  2992  rexrab2  2993  morex  3010  reu2  3014  reu6  3015  reu3  3016  2reuswapdc  3030  2rmorex  3032  cbvrexcsf  3211  ssrexf  3310  rexun  3409  reuss2  3513  reuun2  3516  reupick  3517  reupick3  3518  reximdva0m  3537  rabn0r  3548  rabn0m  3549  r19.2m  3614  r19.2mOLD  3615  r19.9rmv  3619  rexm  3627  rexsns  3747  exsnrex  3750  dfuni2  3935  eluni2  3937  elunirab  3946  iuncom4  4017  iunxiun  4092  intexrabim  4287  bnd2  4308  rexxfrd  4607  elxp2  4790  opeliunxp  4828  xpiundi  4831  xpiundir  4832  rexiunxp  4920  ssrelrn  4970  dmuni  4989  rnmpt  5028  elrnmpt1  5031  elres  5097  dfima2  5126  dfima3  5127  elima2  5130  dfco2a  5286  imaco  5291  imadiflem  5458  imadif  5459  imainlem  5460  imain  5461  funimaexglem  5462  fvelrnb  5747  rexrnmpt  5845  dffo4  5850  dffo5  5851  abrexco  5958  opabex3d  6343  opabex3  6344  abexssex  6347  abexex  6348  ecexr  6805  mapsnd  6963  mapsn  6965  mapsnend  7092  mapsnen  7093  fimax2gtri  7199  ctssdccl  7444  ltexnqq  7768  subhalfnqq  7774  ltbtwnnq  7776  nqnq0  7801  prnmaxl  7848  prnminu  7849  prarloc  7863  genpdflem  7867  genpassl  7884  genpassu  7885  nqprm  7902  nqprl  7911  nqpru  7912  ltsopr  7956  ltexprlemm  7960  ltexprlemloc  7967  suplocexprlemrl  8077  suplocexprlemloc  8081  axprecex  8240  axpre-ltirr  8242  sup3exmid  9280  2rexuz  9964  ioom  10676  nnwosdc  12797  4sqlemafi  13155  inffinp1  13301  omctfn  13315  nninfdclemp1  13322  ptex  13598  fngzsum  13688  gzsumvalx  13689  isbasis2g  15072  tgval2  15078  ntreq0  15159  bdcuni  16819  bj-axun2  16858  dfrals2  17038