Definition df-rex 2461

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 2456	. 2 wff E. x e. A ph
5	2	cv 1352	. . . . 5 class x
6	5, 3	wcel 2148	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1492	. 2 wff E. x ( x e. A /\ ph )
9	4, 8	wb 105	1 wff ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

This definition is referenced by:  ralnex  2465  rexnalim  2466  dfrex2dc  2468  rexbida  2472  rexbidv2  2480  rexbid2  2482  rexbii2  2488  r2exf  2495  risset  2505  nfrexdxy  2511  nfrexdya  2513  nfre1  2520  rexex  2523  rspe  2526  rsp2e  2528  rexim  2571  reximi2  2573  reximdv2  2576  r19.23t  2584  r19.41  2632  r19.43  2635  reean  2646  rexeqf  2670  reu5  2690  rmo5  2693  cbvrexfw  2696  cbvrexf  2698  cbvrexvw  2709  cbvrexdva2  2712  rexv  2756  2gencl  2771  3gencl  2772  rspce  2837  rspcimedv  2844  ceqsrexv  2868  rexab  2900  rexab2  2904  rexrab2  2905  morex  2922  reu2  2926  reu6  2927  reu3  2928  2reuswapdc  2942  2rmorex  2944  cbvrexcsf  3121  ssrexf  3218  rexun  3316  reuss2  3416  reuun2  3419  reupick  3420  reupick3  3421  reximdva0m  3439  rabn0r  3450  rabn0m  3451  r19.2m  3510  r19.2mOLD  3511  r19.9rmv  3515  rexm  3523  rexsns  3632  exsnrex  3635  dfuni2  3812  eluni2  3814  elunirab  3823  iuncom4  3894  iunxiun  3969  intexrabim  4154  bnd2  4174  rexxfrd  4464  elxp2  4645  opeliunxp  4682  xpiundi  4685  xpiundir  4686  rexiunxp  4770  dmuni  4838  rnmpt  4876  elrnmpt1  4879  elres  4944  dfima2  4973  dfima3  4974  elima2  4977  dfco2a  5130  imaco  5135  imadiflem  5296  imadif  5297  imainlem  5298  imain  5299  funimaexglem  5300  fvelrnb  5564  rexrnmpt  5660  dffo4  5665  dffo5  5666  abrexco  5760  opabex3d  6122  opabex3  6123  abexssex  6126  abexex  6127  ecexr  6540  mapsn  6690  mapsnen  6811  fimax2gtri  6901  ctssdccl  7110  ltexnqq  7407  subhalfnqq  7413  ltbtwnnq  7415  nqnq0  7440  prnmaxl  7487  prnminu  7488  prarloc  7502  genpdflem  7506  genpassl  7523  genpassu  7524  nqprm  7541  nqprl  7550  nqpru  7551  ltsopr  7595  ltexprlemm  7599  ltexprlemloc  7606  suplocexprlemrl  7716  suplocexprlemloc  7720  axprecex  7879  axpre-ltirr  7881  sup3exmid  8914  2rexuz  9582  ioom  10261  nnwosdc  12040  inffinp1  12430  omctfn  12444  nninfdclemp1  12451  ptex  12713  isbasis2g  13548  tgval2  13554  ntreq0  13635  bdcuni  14631  bj-axun2  14670