Definition df-rex 2490

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 2485	. 2 wff E. x e. A ph
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2176	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1515	. 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  2494  rexnalim  2495  dfrex2dc  2497  rexbida  2501  rexbidv2  2509  rexbid2  2511  rexbii2  2517  r2exf  2524  risset  2534  nfrexdxy  2540  nfrexdya  2542  nfre1  2549  rexex  2552  rspe  2555  rsp2e  2557  rexim  2600  reximi2  2602  reximdv2  2605  r19.23t  2613  r19.41  2661  r19.43  2664  reean  2675  rexeqf  2699  reu5  2723  rmo5  2726  cbvrexfw  2729  cbvrexf  2731  cbvrexvw  2743  cbvrexdva2  2746  rexv  2790  2gencl  2805  3gencl  2806  rspce  2872  rspcimedv  2879  ceqsrexv  2903  rexab  2935  rexab2  2939  rexrab2  2940  morex  2957  reu2  2961  reu6  2962  reu3  2963  2reuswapdc  2977  2rmorex  2979  cbvrexcsf  3157  ssrexf  3255  rexun  3353  reuss2  3453  reuun2  3456  reupick  3457  reupick3  3458  reximdva0m  3476  rabn0r  3487  rabn0m  3488  r19.2m  3547  r19.2mOLD  3548  r19.9rmv  3552  rexm  3560  rexsns  3672  exsnrex  3675  dfuni2  3852  eluni2  3854  elunirab  3863  iuncom4  3934  iunxiun  4009  intexrabim  4197  bnd2  4217  rexxfrd  4510  elxp2  4693  opeliunxp  4730  xpiundi  4733  xpiundir  4734  rexiunxp  4820  dmuni  4888  rnmpt  4926  elrnmpt1  4929  elres  4995  dfima2  5024  dfima3  5025  elima2  5028  dfco2a  5183  imaco  5188  imadiflem  5353  imadif  5354  imainlem  5355  imain  5356  funimaexglem  5357  fvelrnb  5626  rexrnmpt  5723  dffo4  5728  dffo5  5729  abrexco  5828  opabex3d  6206  opabex3  6207  abexssex  6210  abexex  6211  ecexr  6625  mapsn  6777  mapsnen  6903  fimax2gtri  6998  ctssdccl  7213  ltexnqq  7521  subhalfnqq  7527  ltbtwnnq  7529  nqnq0  7554  prnmaxl  7601  prnminu  7602  prarloc  7616  genpdflem  7620  genpassl  7637  genpassu  7638  nqprm  7655  nqprl  7664  nqpru  7665  ltsopr  7709  ltexprlemm  7713  ltexprlemloc  7720  suplocexprlemrl  7830  suplocexprlemloc  7834  axprecex  7993  axpre-ltirr  7995  sup3exmid  9030  2rexuz  9703  ioom  10403  nnwosdc  12360  4sqlemafi  12718  inffinp1  12800  omctfn  12814  nninfdclemp1  12821  ptex  13096  fngsum  13220  igsumvalx  13221  isbasis2g  14517  tgval2  14523  ntreq0  14604  bdcuni  15812  bj-axun2  15851