Definition df-rex 2396

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 2391	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1313	. . . . 5 class 𝑥
6	5, 3	wcel 1463	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1451	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 104	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  2400  rexnalim  2401  dfrex2dc  2402  rexbida  2406  rexbidv2  2414  rexbii2  2420  r2exf  2427  risset  2437  nfrexdxy  2442  nfrexdya  2444  nfre1  2450  rexex  2453  rspe  2455  rsp2e  2457  rexim  2500  reximi2  2502  reximdv2  2505  r19.23t  2513  r19.41  2560  r19.43  2563  reean  2573  rexeqf  2597  reu5  2617  rmo5  2620  cbvrexf  2623  cbvrexdva2  2633  rexv  2675  2gencl  2690  3gencl  2691  rspce  2755  rspcimedv  2762  ceqsrexv  2785  rexab  2815  rexab2  2819  rexrab2  2820  morex  2837  reu2  2841  reu6  2842  reu3  2843  2reuswapdc  2857  2rmorex  2859  cbvrexcsf  3029  ssrexf  3125  rexun  3222  reuss2  3322  reuun2  3325  reupick  3326  reupick3  3327  reximdva0m  3344  rabn0r  3355  rabn0m  3356  r19.2m  3415  r19.2mOLD  3416  r19.9rmv  3420  rexm  3428  rexsns  3529  exsnrex  3532  dfuni2  3704  eluni2  3706  elunirab  3715  iuncom4  3786  iunxiun  3860  intexrabim  4038  bnd2  4057  rexxfrd  4344  elxp2  4517  opeliunxp  4554  xpiundi  4557  xpiundir  4558  rexiunxp  4641  dmuni  4709  rnmpt  4747  elrnmpt1  4750  elres  4813  dfima2  4841  dfima3  4842  elima2  4845  dfco2a  4997  imaco  5002  imadiflem  5160  imadif  5161  imainlem  5162  imain  5163  funimaexglem  5164  fvelrnb  5423  rexrnmpt  5517  dffo4  5522  dffo5  5523  abrexco  5614  opabex3d  5973  opabex3  5974  abexssex  5977  abexex  5978  ecexr  6388  mapsn  6538  mapsnen  6659  fimax2gtri  6748  ctssdccl  6948  ltexnqq  7164  subhalfnqq  7170  ltbtwnnq  7172  nqnq0  7197  prnmaxl  7244  prnminu  7245  prarloc  7259  genpdflem  7263  genpassl  7280  genpassu  7281  nqprm  7298  nqprl  7307  nqpru  7308  ltsopr  7352  ltexprlemm  7356  ltexprlemloc  7363  axprecex  7615  axpre-ltirr  7617  sup3exmid  8625  2rexuz  9279  ioom  9931  inffinp1  11787  isbasis2g  12055  tgval2  12063  ntreq0  12144  bdcuni  12764  bj-axun2  12803