Definition df-rex 2461

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 2456	. 2 wff E. x e. A ph
5	2	cv 1352	. . . . 5 class x
6	5, 3	wcel 2148	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1492	. 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  2465  rexnalim  2466  dfrex2dc  2468  rexbida  2472  rexbidv2  2480  rexbid2  2482  rexbii2  2488  r2exf  2495  risset  2505  nfrexdxy  2511  nfrexdya  2513  nfre1  2520  rexex  2523  rspe  2526  rsp2e  2528  rexim  2571  reximi2  2573  reximdv2  2576  r19.23t  2584  r19.41  2632  r19.43  2635  reean  2645  rexeqf  2669  reu5  2689  rmo5  2692  cbvrexfw  2695  cbvrexf  2697  cbvrexvw  2708  cbvrexdva2  2711  rexv  2755  2gencl  2770  3gencl  2771  rspce  2836  rspcimedv  2843  ceqsrexv  2867  rexab  2899  rexab2  2903  rexrab2  2904  morex  2921  reu2  2925  reu6  2926  reu3  2927  2reuswapdc  2941  2rmorex  2943  cbvrexcsf  3120  ssrexf  3217  rexun  3315  reuss2  3415  reuun2  3418  reupick  3419  reupick3  3420  reximdva0m  3438  rabn0r  3449  rabn0m  3450  r19.2m  3509  r19.2mOLD  3510  r19.9rmv  3514  rexm  3522  rexsns  3631  exsnrex  3634  dfuni2  3811  eluni2  3813  elunirab  3822  iuncom4  3893  iunxiun  3968  intexrabim  4153  bnd2  4173  rexxfrd  4463  elxp2  4644  opeliunxp  4681  xpiundi  4684  xpiundir  4685  rexiunxp  4769  dmuni  4837  rnmpt  4875  elrnmpt1  4878  elres  4943  dfima2  4972  dfima3  4973  elima2  4976  dfco2a  5129  imaco  5134  imadiflem  5295  imadif  5296  imainlem  5297  imain  5298  funimaexglem  5299  fvelrnb  5563  rexrnmpt  5659  dffo4  5664  dffo5  5665  abrexco  5759  opabex3d  6121  opabex3  6122  abexssex  6125  abexex  6126  ecexr  6539  mapsn  6689  mapsnen  6810  fimax2gtri  6900  ctssdccl  7109  ltexnqq  7406  subhalfnqq  7412  ltbtwnnq  7414  nqnq0  7439  prnmaxl  7486  prnminu  7487  prarloc  7501  genpdflem  7505  genpassl  7522  genpassu  7523  nqprm  7540  nqprl  7549  nqpru  7550  ltsopr  7594  ltexprlemm  7598  ltexprlemloc  7605  suplocexprlemrl  7715  suplocexprlemloc  7719  axprecex  7878  axpre-ltirr  7880  sup3exmid  8912  2rexuz  9580  ioom  10258  nnwosdc  12034  inffinp1  12424  omctfn  12438  nninfdclemp1  12445  ptex  12707  isbasis2g  13476  tgval2  13482  ntreq0  13563  bdcuni  14548  bj-axun2  14587