Definition df-rex 2478

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 2473	. 2 wff E. x e. A ph
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2164	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1503	. 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  2482  rexnalim  2483  dfrex2dc  2485  rexbida  2489  rexbidv2  2497  rexbid2  2499  rexbii2  2505  r2exf  2512  risset  2522  nfrexdxy  2528  nfrexdya  2530  nfre1  2537  rexex  2540  rspe  2543  rsp2e  2545  rexim  2588  reximi2  2590  reximdv2  2593  r19.23t  2601  r19.41  2649  r19.43  2652  reean  2663  rexeqf  2687  reu5  2711  rmo5  2714  cbvrexfw  2717  cbvrexf  2719  cbvrexvw  2731  cbvrexdva2  2734  rexv  2778  2gencl  2793  3gencl  2794  rspce  2860  rspcimedv  2867  ceqsrexv  2891  rexab  2923  rexab2  2927  rexrab2  2928  morex  2945  reu2  2949  reu6  2950  reu3  2951  2reuswapdc  2965  2rmorex  2967  cbvrexcsf  3145  ssrexf  3242  rexun  3340  reuss2  3440  reuun2  3443  reupick  3444  reupick3  3445  reximdva0m  3463  rabn0r  3474  rabn0m  3475  r19.2m  3534  r19.2mOLD  3535  r19.9rmv  3539  rexm  3547  rexsns  3658  exsnrex  3661  dfuni2  3838  eluni2  3840  elunirab  3849  iuncom4  3920  iunxiun  3995  intexrabim  4183  bnd2  4203  rexxfrd  4495  elxp2  4678  opeliunxp  4715  xpiundi  4718  xpiundir  4719  rexiunxp  4805  dmuni  4873  rnmpt  4911  elrnmpt1  4914  elres  4979  dfima2  5008  dfima3  5009  elima2  5012  dfco2a  5167  imaco  5172  imadiflem  5334  imadif  5335  imainlem  5336  imain  5337  funimaexglem  5338  fvelrnb  5605  rexrnmpt  5702  dffo4  5707  dffo5  5708  abrexco  5803  opabex3d  6175  opabex3  6176  abexssex  6179  abexex  6180  ecexr  6594  mapsn  6746  mapsnen  6867  fimax2gtri  6959  ctssdccl  7172  ltexnqq  7470  subhalfnqq  7476  ltbtwnnq  7478  nqnq0  7503  prnmaxl  7550  prnminu  7551  prarloc  7565  genpdflem  7569  genpassl  7586  genpassu  7587  nqprm  7604  nqprl  7613  nqpru  7614  ltsopr  7658  ltexprlemm  7662  ltexprlemloc  7669  suplocexprlemrl  7779  suplocexprlemloc  7783  axprecex  7942  axpre-ltirr  7944  sup3exmid  8978  2rexuz  9650  ioom  10332  nnwosdc  12179  4sqlemafi  12536  inffinp1  12589  omctfn  12603  nninfdclemp1  12610  ptex  12878  fngsum  12974  igsumvalx  12975  isbasis2g  14224  tgval2  14230  ntreq0  14311  bdcuni  15428  bj-axun2  15467