Definition df-rex 2454

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 2449	. 2 wff E. x e. A ph
5	2	cv 1347	. . . . 5 class x
6	5, 3	wcel 2141	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1485	. 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  2458  rexnalim  2459  dfrex2dc  2461  rexbida  2465  rexbidv2  2473  rexbid2  2475  rexbii2  2481  r2exf  2488  risset  2498  nfrexdxy  2504  nfrexdya  2506  nfre1  2513  rexex  2516  rspe  2519  rsp2e  2521  rexim  2564  reximi2  2566  reximdv2  2569  r19.23t  2577  r19.41  2625  r19.43  2628  reean  2638  rexeqf  2662  reu5  2682  rmo5  2685  cbvrexfw  2688  cbvrexf  2690  cbvrexvw  2701  cbvrexdva2  2704  rexv  2748  2gencl  2763  3gencl  2764  rspce  2829  rspcimedv  2836  ceqsrexv  2860  rexab  2892  rexab2  2896  rexrab2  2897  morex  2914  reu2  2918  reu6  2919  reu3  2920  2reuswapdc  2934  2rmorex  2936  cbvrexcsf  3112  ssrexf  3209  rexun  3307  reuss2  3407  reuun2  3410  reupick  3411  reupick3  3412  reximdva0m  3430  rabn0r  3441  rabn0m  3442  r19.2m  3501  r19.2mOLD  3502  r19.9rmv  3506  rexm  3514  rexsns  3622  exsnrex  3625  dfuni2  3798  eluni2  3800  elunirab  3809  iuncom4  3880  iunxiun  3954  intexrabim  4139  bnd2  4159  rexxfrd  4448  elxp2  4629  opeliunxp  4666  xpiundi  4669  xpiundir  4670  rexiunxp  4753  dmuni  4821  rnmpt  4859  elrnmpt1  4862  elres  4927  dfima2  4955  dfima3  4956  elima2  4959  dfco2a  5111  imaco  5116  imadiflem  5277  imadif  5278  imainlem  5279  imain  5280  funimaexglem  5281  fvelrnb  5544  rexrnmpt  5639  dffo4  5644  dffo5  5645  abrexco  5738  opabex3d  6100  opabex3  6101  abexssex  6104  abexex  6105  ecexr  6518  mapsn  6668  mapsnen  6789  fimax2gtri  6879  ctssdccl  7088  ltexnqq  7370  subhalfnqq  7376  ltbtwnnq  7378  nqnq0  7403  prnmaxl  7450  prnminu  7451  prarloc  7465  genpdflem  7469  genpassl  7486  genpassu  7487  nqprm  7504  nqprl  7513  nqpru  7514  ltsopr  7558  ltexprlemm  7562  ltexprlemloc  7569  suplocexprlemrl  7679  suplocexprlemloc  7683  axprecex  7842  axpre-ltirr  7844  sup3exmid  8873  2rexuz  9541  ioom  10217  nnwosdc  11994  inffinp1  12384  omctfn  12398  nninfdclemp1  12405  isbasis2g  12837  tgval2  12845  ntreq0  12926  bdcuni  13911  bj-axun2  13950