Definition df-rex 2441

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 2436	. 2 wff E. x e. A ph
5	2	cv 1334	. . . . 5 class x
6	5, 3	wcel 2128	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1472	. 2 wff E. x ( x e. A /\ ph )
9	4, 8	wb 104	1 wff ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

This definition is referenced by:  ralnex  2445  rexnalim  2446  dfrex2dc  2448  rexbida  2452  rexbidv2  2460  rexbid2  2462  rexbii2  2468  r2exf  2475  risset  2485  nfrexdxy  2491  nfrexdya  2493  nfre1  2500  rexex  2503  rspe  2506  rsp2e  2508  rexim  2551  reximi2  2553  reximdv2  2556  r19.23t  2564  r19.41  2612  r19.43  2615  reean  2625  rexeqf  2649  reu5  2669  rmo5  2672  cbvrexf  2675  cbvrexvw  2685  cbvrexdva2  2688  rexv  2730  2gencl  2745  3gencl  2746  rspce  2811  rspcimedv  2818  ceqsrexv  2842  rexab  2874  rexab2  2878  rexrab2  2879  morex  2896  reu2  2900  reu6  2901  reu3  2902  2reuswapdc  2916  2rmorex  2918  cbvrexcsf  3094  ssrexf  3190  rexun  3287  reuss2  3387  reuun2  3390  reupick  3391  reupick3  3392  reximdva0m  3409  rabn0r  3420  rabn0m  3421  r19.2m  3480  r19.2mOLD  3481  r19.9rmv  3485  rexm  3493  rexsns  3598  exsnrex  3601  dfuni2  3774  eluni2  3776  elunirab  3785  iuncom4  3856  iunxiun  3930  intexrabim  4114  bnd2  4134  rexxfrd  4422  elxp2  4603  opeliunxp  4640  xpiundi  4643  xpiundir  4644  rexiunxp  4727  dmuni  4795  rnmpt  4833  elrnmpt1  4836  elres  4901  dfima2  4929  dfima3  4930  elima2  4933  dfco2a  5085  imaco  5090  imadiflem  5248  imadif  5249  imainlem  5250  imain  5251  funimaexglem  5252  fvelrnb  5515  rexrnmpt  5609  dffo4  5614  dffo5  5615  abrexco  5706  opabex3d  6066  opabex3  6067  abexssex  6070  abexex  6071  ecexr  6482  mapsn  6632  mapsnen  6753  fimax2gtri  6843  ctssdccl  7049  ltexnqq  7322  subhalfnqq  7328  ltbtwnnq  7330  nqnq0  7355  prnmaxl  7402  prnminu  7403  prarloc  7417  genpdflem  7421  genpassl  7438  genpassu  7439  nqprm  7456  nqprl  7465  nqpru  7466  ltsopr  7510  ltexprlemm  7514  ltexprlemloc  7521  suplocexprlemrl  7631  suplocexprlemloc  7635  axprecex  7794  axpre-ltirr  7796  sup3exmid  8822  2rexuz  9487  ioom  10153  inffinp1  12141  omctfn  12155  isbasis2g  12414  tgval2  12422  ntreq0  12503  bdcuni  13422  bj-axun2  13461