Definition df-rex 2514

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 2509	. 2 wff E. x e. A ph
5	2	cv 1394	. . . . 5 class x
6	5, 3	wcel 2200	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1538	. 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  2518  rexnalim  2519  dfrex2dc  2521  rexbida  2525  rexbidv2  2533  rexbid2  2535  rexbii2  2541  r2exf  2548  risset  2558  nfrexdxy  2564  nfrexdya  2566  nfre1  2573  rexex  2576  rspe  2579  rsp2e  2581  rexim  2624  reximi2  2626  reximdv2  2629  r19.23t  2638  r19.41  2686  r19.43  2689  reean  2700  rexeqf  2725  reu5  2749  rmo5  2752  cbvrexfw  2755  cbvrexf  2757  cbvrexvw  2770  cbvrexdva2  2773  rexv  2818  2gencl  2833  3gencl  2834  rspce  2902  rspcimedv  2909  ceqsrexv  2933  rexab  2965  rexab2  2969  rexrab2  2970  morex  2987  reu2  2991  reu6  2992  reu3  2993  2reuswapdc  3007  2rmorex  3009  cbvrexcsf  3188  ssrexf  3286  rexun  3384  reuss2  3484  reuun2  3487  reupick  3488  reupick3  3489  reximdva0m  3507  rabn0r  3518  rabn0m  3519  r19.2m  3578  r19.2mOLD  3579  r19.9rmv  3583  rexm  3591  rexsns  3705  exsnrex  3708  dfuni2  3890  eluni2  3892  elunirab  3901  iuncom4  3972  iunxiun  4047  intexrabim  4237  bnd2  4257  rexxfrd  4554  elxp2  4737  opeliunxp  4774  xpiundi  4777  xpiundir  4778  rexiunxp  4864  ssrelrn  4914  dmuni  4933  rnmpt  4972  elrnmpt1  4975  elres  5041  dfima2  5070  dfima3  5071  elima2  5074  dfco2a  5229  imaco  5234  imadiflem  5400  imadif  5401  imainlem  5402  imain  5403  funimaexglem  5404  fvelrnb  5683  rexrnmpt  5780  dffo4  5785  dffo5  5786  abrexco  5889  opabex3d  6272  opabex3  6273  abexssex  6276  abexex  6277  ecexr  6693  mapsn  6845  mapsnen  6972  fimax2gtri  7072  ctssdccl  7289  ltexnqq  7606  subhalfnqq  7612  ltbtwnnq  7614  nqnq0  7639  prnmaxl  7686  prnminu  7687  prarloc  7701  genpdflem  7705  genpassl  7722  genpassu  7723  nqprm  7740  nqprl  7749  nqpru  7750  ltsopr  7794  ltexprlemm  7798  ltexprlemloc  7805  suplocexprlemrl  7915  suplocexprlemloc  7919  axprecex  8078  axpre-ltirr  8080  sup3exmid  9115  2rexuz  9789  ioom  10492  nnwosdc  12576  4sqlemafi  12934  inffinp1  13016  omctfn  13030  nninfdclemp1  13037  ptex  13313  fngsum  13437  igsumvalx  13438  isbasis2g  14735  tgval2  14741  ntreq0  14822  bdcuni  16322  bj-axun2  16361