Definition df-rex 2528

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 2523	. 2 wff E. x e. A ph
5	2	cv 1397	. . . . 5 class x
6	5, 3	wcel 2205	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1541	. 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  2532  rexnalim  2533  dfrex2dc  2535  rexbida  2539  rexbidv2  2547  rexbid2  2549  rexbii2  2555  r2exf  2562  risset  2572  nfrexdxy  2578  nfrexdya  2580  nfre1  2587  rexex  2590  rspe  2593  rsp2e  2595  rexim  2638  reximi2  2640  reximdv2  2643  r19.23t  2652  r19.41  2700  r19.43  2703  reean  2714  rexeqf  2740  reu5  2764  rmo5  2767  cbvrexfw  2770  cbvrexf  2772  cbvrexvw  2785  cbvrexdva2  2788  rexv  2834  2gencl  2849  3gencl  2850  rspce  2918  rspcimedv  2925  ceqsrexv  2949  rexab  2981  rexab2  2985  rexrab2  2986  morex  3003  reu2  3007  reu6  3008  reu3  3009  2reuswapdc  3023  2rmorex  3025  cbvrexcsf  3204  ssrexf  3302  rexun  3401  reuss2  3503  reuun2  3506  reupick  3507  reupick3  3508  reximdva0m  3526  rabn0r  3537  rabn0m  3538  r19.2m  3598  r19.2mOLD  3599  r19.9rmv  3603  rexm  3611  rexsns  3730  exsnrex  3733  dfuni2  3918  eluni2  3920  elunirab  3929  iuncom4  4000  iunxiun  4075  intexrabim  4267  bnd2  4288  rexxfrd  4586  elxp2  4769  opeliunxp  4807  xpiundi  4810  xpiundir  4811  rexiunxp  4899  ssrelrn  4949  dmuni  4968  rnmpt  5007  elrnmpt1  5010  elres  5076  dfima2  5105  dfima3  5106  elima2  5109  dfco2a  5265  imaco  5270  imadiflem  5437  imadif  5438  imainlem  5439  imain  5440  funimaexglem  5441  fvelrnb  5726  rexrnmpt  5822  dffo4  5827  dffo5  5828  abrexco  5934  opabex3d  6316  opabex3  6317  abexssex  6320  abexex  6321  ecexr  6774  mapsnd  6925  mapsn  6927  mapsnend  7054  mapsnen  7055  fimax2gtri  7161  ctssdccl  7404  ltexnqq  7725  subhalfnqq  7731  ltbtwnnq  7733  nqnq0  7758  prnmaxl  7805  prnminu  7806  prarloc  7820  genpdflem  7824  genpassl  7841  genpassu  7842  nqprm  7859  nqprl  7868  nqpru  7869  ltsopr  7913  ltexprlemm  7917  ltexprlemloc  7924  suplocexprlemrl  8034  suplocexprlemloc  8038  axprecex  8197  axpre-ltirr  8199  sup3exmid  9233  2rexuz  9917  ioom  10624  nnwosdc  12739  4sqlemafi  13097  inffinp1  13197  omctfn  13211  nninfdclemp1  13218  ptex  13494  fngsum  13618  igsumvalx  13619  isbasis2g  14927  tgval2  14933  ntreq0  15014  bdcuni  16663  bj-axun2  16702