Definition df-rex 2422

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 2417	. 2 wff E. x e. A ph
5	2	cv 1330	. . . . 5 class x
6	5, 3	wcel 1480	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1468	. 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  2426  rexnalim  2427  dfrex2dc  2428  rexbida  2432  rexbidv2  2440  rexbii2  2446  r2exf  2453  risset  2463  nfrexdxy  2468  nfrexdya  2470  nfre1  2476  rexex  2479  rspe  2481  rsp2e  2483  rexim  2526  reximi2  2528  reximdv2  2531  r19.23t  2539  r19.41  2586  r19.43  2589  reean  2599  rexeqf  2623  reu5  2643  rmo5  2646  cbvrexf  2649  cbvrexdva2  2662  rexv  2704  2gencl  2719  3gencl  2720  rspce  2784  rspcimedv  2791  ceqsrexv  2815  rexab  2846  rexab2  2850  rexrab2  2851  morex  2868  reu2  2872  reu6  2873  reu3  2874  2reuswapdc  2888  2rmorex  2890  cbvrexcsf  3063  ssrexf  3159  rexun  3256  reuss2  3356  reuun2  3359  reupick  3360  reupick3  3361  reximdva0m  3378  rabn0r  3389  rabn0m  3390  r19.2m  3449  r19.2mOLD  3450  r19.9rmv  3454  rexm  3462  rexsns  3563  exsnrex  3566  dfuni2  3738  eluni2  3740  elunirab  3749  iuncom4  3820  iunxiun  3894  intexrabim  4078  bnd2  4097  rexxfrd  4384  elxp2  4557  opeliunxp  4594  xpiundi  4597  xpiundir  4598  rexiunxp  4681  dmuni  4749  rnmpt  4787  elrnmpt1  4790  elres  4855  dfima2  4883  dfima3  4884  elima2  4887  dfco2a  5039  imaco  5044  imadiflem  5202  imadif  5203  imainlem  5204  imain  5205  funimaexglem  5206  fvelrnb  5469  rexrnmpt  5563  dffo4  5568  dffo5  5569  abrexco  5660  opabex3d  6019  opabex3  6020  abexssex  6023  abexex  6024  ecexr  6434  mapsn  6584  mapsnen  6705  fimax2gtri  6795  ctssdccl  6996  ltexnqq  7216  subhalfnqq  7222  ltbtwnnq  7224  nqnq0  7249  prnmaxl  7296  prnminu  7297  prarloc  7311  genpdflem  7315  genpassl  7332  genpassu  7333  nqprm  7350  nqprl  7359  nqpru  7360  ltsopr  7404  ltexprlemm  7408  ltexprlemloc  7415  suplocexprlemrl  7525  suplocexprlemloc  7529  axprecex  7688  axpre-ltirr  7690  sup3exmid  8715  2rexuz  9377  ioom  10038  inffinp1  11942  isbasis2g  12212  tgval2  12220  ntreq0  12301  bdcuni  13074  bj-axun2  13113