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  3889  eluni2  3891  elunirab  3900  iuncom4  3971  iunxiun  4046  intexrabim  4236  bnd2  4256  rexxfrd  4553  elxp2  4736  opeliunxp  4773  xpiundi  4776  xpiundir  4777  rexiunxp  4863  ssrelrn  4913  dmuni  4932  rnmpt  4971  elrnmpt1  4974  elres  5040  dfima2  5069  dfima3  5070  elima2  5073  dfco2a  5228  imaco  5233  imadiflem  5399  imadif  5400  imainlem  5401  imain  5402  funimaexglem  5403  fvelrnb  5680  rexrnmpt  5777  dffo4  5782  dffo5  5783  abrexco  5882  opabex3d  6264  opabex3  6265  abexssex  6268  abexex  6269  ecexr  6683  mapsn  6835  mapsnen  6962  fimax2gtri  7059  ctssdccl  7274  ltexnqq  7591  subhalfnqq  7597  ltbtwnnq  7599  nqnq0  7624  prnmaxl  7671  prnminu  7672  prarloc  7686  genpdflem  7690  genpassl  7707  genpassu  7708  nqprm  7725  nqprl  7734  nqpru  7735  ltsopr  7779  ltexprlemm  7783  ltexprlemloc  7790  suplocexprlemrl  7900  suplocexprlemloc  7904  axprecex  8063  axpre-ltirr  8065  sup3exmid  9100  2rexuz  9773  ioom  10475  nnwosdc  12555  4sqlemafi  12913  inffinp1  12995  omctfn  13009  nninfdclemp1  13016  ptex  13292  fngsum  13416  igsumvalx  13417  isbasis2g  14713  tgval2  14719  ntreq0  14800  bdcuni  16197  bj-axun2  16236