Definition df-rex 2489

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 2484	. 2 wff E. x e. A ph
5	2	cv 1371	. . . . 5 class x
6	5, 3	wcel 2175	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1514	. 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  2493  rexnalim  2494  dfrex2dc  2496  rexbida  2500  rexbidv2  2508  rexbid2  2510  rexbii2  2516  r2exf  2523  risset  2533  nfrexdxy  2539  nfrexdya  2541  nfre1  2548  rexex  2551  rspe  2554  rsp2e  2556  rexim  2599  reximi2  2601  reximdv2  2604  r19.23t  2612  r19.41  2660  r19.43  2663  reean  2674  rexeqf  2698  reu5  2722  rmo5  2725  cbvrexfw  2728  cbvrexf  2730  cbvrexvw  2742  cbvrexdva2  2745  rexv  2789  2gencl  2804  3gencl  2805  rspce  2871  rspcimedv  2878  ceqsrexv  2902  rexab  2934  rexab2  2938  rexrab2  2939  morex  2956  reu2  2960  reu6  2961  reu3  2962  2reuswapdc  2976  2rmorex  2978  cbvrexcsf  3156  ssrexf  3254  rexun  3352  reuss2  3452  reuun2  3455  reupick  3456  reupick3  3457  reximdva0m  3475  rabn0r  3486  rabn0m  3487  r19.2m  3546  r19.2mOLD  3547  r19.9rmv  3551  rexm  3559  rexsns  3671  exsnrex  3674  dfuni2  3851  eluni2  3853  elunirab  3862  iuncom4  3933  iunxiun  4008  intexrabim  4196  bnd2  4216  rexxfrd  4509  elxp2  4692  opeliunxp  4729  xpiundi  4732  xpiundir  4733  rexiunxp  4819  dmuni  4887  rnmpt  4925  elrnmpt1  4928  elres  4994  dfima2  5023  dfima3  5024  elima2  5027  dfco2a  5182  imaco  5187  imadiflem  5352  imadif  5353  imainlem  5354  imain  5355  funimaexglem  5356  fvelrnb  5625  rexrnmpt  5722  dffo4  5727  dffo5  5728  abrexco  5827  opabex3d  6205  opabex3  6206  abexssex  6209  abexex  6210  ecexr  6624  mapsn  6776  mapsnen  6902  fimax2gtri  6997  ctssdccl  7212  ltexnqq  7520  subhalfnqq  7526  ltbtwnnq  7528  nqnq0  7553  prnmaxl  7600  prnminu  7601  prarloc  7615  genpdflem  7619  genpassl  7636  genpassu  7637  nqprm  7654  nqprl  7663  nqpru  7664  ltsopr  7708  ltexprlemm  7712  ltexprlemloc  7719  suplocexprlemrl  7829  suplocexprlemloc  7833  axprecex  7992  axpre-ltirr  7994  sup3exmid  9029  2rexuz  9702  ioom  10401  nnwosdc  12302  4sqlemafi  12660  inffinp1  12742  omctfn  12756  nninfdclemp1  12763  ptex  13038  fngsum  13162  igsumvalx  13163  isbasis2g  14459  tgval2  14465  ntreq0  14546  bdcuni  15745  bj-axun2  15784