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 used 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  3748  exsnrex  3751  dfuni2  3937  eluni2  3939  elunirab  3948  iuncom4  4019  iunxiun  4094  intexrabim  4291  bnd2  4312  rexxfrd  4611  elxp2  4794  opeliunxp  4832  xpiundi  4835  xpiundir  4836  rexiunxp  4924  ssrelrn  4974  dmuni  4993  rnmpt  5032  elrnmpt1  5035  elres  5101  dfima2  5131  dfima3  5132  elima2  5135  dfco2a  5291  imaco  5296  imadiflem  5463  imadif  5464  imainlem  5465  imain  5466  funimaexglem  5467  fvelrnb  5753  rexrnmpt  5854  dffo4  5859  dffo5  5860  abrexco  5968  opabex3d  6354  opabex3  6355  abexssex  6358  abexex  6359  ecexr  6816  mapsnd  6974  mapsn  6976  mapsnend  7103  mapsnen  7104  fimax2gtri  7210  ctssdccl  7457  ltexnqq  7781  subhalfnqq  7787  ltbtwnnq  7789  nqnq0  7814  prnmaxl  7861  prnminu  7862  prarloc  7876  genpdflem  7880  genpassl  7897  genpassu  7898  nqprm  7915  nqprl  7924  nqpru  7925  ltsopr  7969  ltexprlemm  7973  ltexprlemloc  7980  suplocexprlemrl  8090  suplocexprlemloc  8094  axprecex  8253  axpre-ltirr  8255  sup3exmid  9295  2rexuz  9998  ioom  10712  nnwosdc  12841  4sqlemafi  13203  inffinp1  13378  omctfn  13392  nninfdclemp1  13399  ptex  13677  fngzsum  13767  gzsumvalx  13768  isbasis2g  15271  tgval2  15277  ntreq0  15358  bdcuni  17107  bj-axun2  17146  dfrals2  17337