Definition df-rex 2534

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 2529	. 2 wff E. x e. A ph
5	2	cv 1401	. . . . 5 class x
6	5, 3	wcel 2209	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1545	. 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 used by:  ralnex  2538  rexnalim  2539  dfrex2dc  2541  rexbida  2545  rexbidv2  2553  rexbid2  2555  rexbii2  2561  r2exf  2568  risset  2578  nfrexdxy  2584  nfrexdya  2586  nfre1  2593  rexex  2596  rspe  2599  rsp2e  2601  rexim  2644  reximi2  2646  reximdv2  2649  r19.23t  2658  r19.41  2706  r19.43  2709  reean  2720  rexeqf  2746  reu5  2770  rmo5  2773  cbvrexfw  2776  cbvrexf  2778  cbvrexvw  2791  cbvrexdva2  2794  rexv  2840  2gencl  2855  3gencl  2856  rspce  2924  rspcimedv  2931  ceqsrexv  2956  rexab  2988  rexab2  2992  rexrab2  2993  morex  3010  reu2  3014  reu6  3015  reu3  3016  2reuswapdc  3030  2rmorex  3032  cbvrexcsf  3211  ssrexf  3310  rexun  3409  reuss2  3513  reuun2  3516  reupick  3517  reupick3  3518  reximdva0m  3537  rabn0r  3548  rabn0m  3549  r19.2m  3614  r19.2mOLD  3615  r19.9rmv  3619  rexm  3627  rexsns  3748  exsnrex  3751  dfuni2  3937  eluni2  3939  elunirab  3948  iuncom4  4019  iunxiun  4094  intexrabim  4289  bnd2  4310  rexxfrd  4609  elxp2  4792  opeliunxp  4830  xpiundi  4833  xpiundir  4834  rexiunxp  4922  ssrelrn  4972  dmuni  4991  rnmpt  5030  elrnmpt1  5033  elres  5099  dfima2  5128  dfima3  5129  elima2  5132  dfco2a  5288  imaco  5293  imadiflem  5460  imadif  5461  imainlem  5462  imain  5463  funimaexglem  5464  fvelrnb  5750  rexrnmpt  5851  dffo4  5856  dffo5  5857  abrexco  5965  opabex3d  6350  opabex3  6351  abexssex  6354  abexex  6355  ecexr  6812  mapsnd  6970  mapsn  6972  mapsnend  7099  mapsnen  7100  fimax2gtri  7206  ctssdccl  7451  ltexnqq  7775  subhalfnqq  7781  ltbtwnnq  7783  nqnq0  7808  prnmaxl  7855  prnminu  7856  prarloc  7870  genpdflem  7874  genpassl  7891  genpassu  7892  nqprm  7909  nqprl  7918  nqpru  7919  ltsopr  7963  ltexprlemm  7967  ltexprlemloc  7974  suplocexprlemrl  8084  suplocexprlemloc  8088  axprecex  8247  axpre-ltirr  8249  sup3exmid  9287  2rexuz  9982  ioom  10695  nnwosdc  12816  4sqlemafi  13174  inffinp1  13320  omctfn  13334  nninfdclemp1  13341  ptex  13618  fngzsum  13708  gzsumvalx  13709  isbasis2g  15146  tgval2  15152  ntreq0  15233  bdcuni  16902  bj-axun2  16941  dfrals2  17130