Definition df-rex 2394

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	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

Detailed syntax breakdown of Definition df-rex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wrex 2389	. 2 wff E. x e. A ph
5	2	cv 1311	. . . . 5 class x
6	5, 3	wcel 1461	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1449	. 2 wff E. x ( x e. A /\ ph )
9	4, 8	wb 104	1 wff ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

This definition is referenced by:  ralnex  2398  rexnalim  2399  dfrex2dc  2400  rexbida  2404  rexbidv2  2412  rexbii2  2418  r2exf  2425  risset  2435  nfrexdxy  2440  nfrexdya  2442  nfre1  2448  rexex  2451  rspe  2453  rsp2e  2455  rexim  2498  reximi2  2500  reximdv2  2503  r19.23t  2511  r19.41  2558  r19.43  2561  reean  2571  rexeqf  2595  reu5  2615  rmo5  2618  cbvrexf  2621  cbvrexdva2  2631  rexv  2673  2gencl  2688  3gencl  2689  rspce  2753  rspcimedv  2760  ceqsrexv  2783  rexab  2813  rexab2  2817  rexrab2  2818  morex  2835  reu2  2839  reu6  2840  reu3  2841  2reuswapdc  2855  2rmorex  2857  cbvrexcsf  3027  ssrexf  3123  rexun  3220  reuss2  3320  reuun2  3323  reupick  3324  reupick3  3325  reximdva0m  3342  rabn0r  3353  rabn0m  3354  r19.2m  3413  r19.2mOLD  3414  r19.9rmv  3418  rexm  3426  rexsns  3527  exsnrex  3530  dfuni2  3702  eluni2  3704  elunirab  3713  iuncom4  3784  iunxiun  3858  intexrabim  4036  bnd2  4055  rexxfrd  4342  elxp2  4515  opeliunxp  4552  xpiundi  4555  xpiundir  4556  rexiunxp  4639  dmuni  4707  rnmpt  4745  elrnmpt1  4748  elres  4811  dfima2  4839  dfima3  4840  elima2  4843  dfco2a  4995  imaco  5000  imadiflem  5158  imadif  5159  imainlem  5160  imain  5161  funimaexglem  5162  fvelrnb  5421  rexrnmpt  5515  dffo4  5520  dffo5  5521  abrexco  5612  opabex3d  5971  opabex3  5972  abexssex  5975  abexex  5976  ecexr  6386  mapsn  6536  mapsnen  6657  fimax2gtri  6746  ctssdccl  6946  ltexnqq  7158  subhalfnqq  7164  ltbtwnnq  7166  nqnq0  7191  prnmaxl  7238  prnminu  7239  prarloc  7253  genpdflem  7257  genpassl  7274  genpassu  7275  nqprm  7292  nqprl  7301  nqpru  7302  ltsopr  7346  ltexprlemm  7350  ltexprlemloc  7357  axprecex  7609  axpre-ltirr  7611  sup3exmid  8619  2rexuz  9273  ioom  9925  inffinp1  11781  isbasis2g  12049  tgval2  12057  ntreq0  12138  bdcuni  12757  bj-axun2  12796