Definition df-rex 2492

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 2487	. 2 wff E. x e. A ph
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2178	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1516	. 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  2496  rexnalim  2497  dfrex2dc  2499  rexbida  2503  rexbidv2  2511  rexbid2  2513  rexbii2  2519  r2exf  2526  risset  2536  nfrexdxy  2542  nfrexdya  2544  nfre1  2551  rexex  2554  rspe  2557  rsp2e  2559  rexim  2602  reximi2  2604  reximdv2  2607  r19.23t  2615  r19.41  2663  r19.43  2666  reean  2677  rexeqf  2702  reu5  2726  rmo5  2729  cbvrexfw  2732  cbvrexf  2734  cbvrexvw  2747  cbvrexdva2  2750  rexv  2795  2gencl  2810  3gencl  2811  rspce  2879  rspcimedv  2886  ceqsrexv  2910  rexab  2942  rexab2  2946  rexrab2  2947  morex  2964  reu2  2968  reu6  2969  reu3  2970  2reuswapdc  2984  2rmorex  2986  cbvrexcsf  3165  ssrexf  3263  rexun  3361  reuss2  3461  reuun2  3464  reupick  3465  reupick3  3466  reximdva0m  3484  rabn0r  3495  rabn0m  3496  r19.2m  3555  r19.2mOLD  3556  r19.9rmv  3560  rexm  3568  rexsns  3682  exsnrex  3685  dfuni2  3866  eluni2  3868  elunirab  3877  iuncom4  3948  iunxiun  4023  intexrabim  4213  bnd2  4233  rexxfrd  4528  elxp2  4711  opeliunxp  4748  xpiundi  4751  xpiundir  4752  rexiunxp  4838  ssrelrn  4888  dmuni  4907  rnmpt  4945  elrnmpt1  4948  elres  5014  dfima2  5043  dfima3  5044  elima2  5047  dfco2a  5202  imaco  5207  imadiflem  5372  imadif  5373  imainlem  5374  imain  5375  funimaexglem  5376  fvelrnb  5649  rexrnmpt  5746  dffo4  5751  dffo5  5752  abrexco  5851  opabex3d  6229  opabex3  6230  abexssex  6233  abexex  6234  ecexr  6648  mapsn  6800  mapsnen  6927  fimax2gtri  7024  ctssdccl  7239  ltexnqq  7556  subhalfnqq  7562  ltbtwnnq  7564  nqnq0  7589  prnmaxl  7636  prnminu  7637  prarloc  7651  genpdflem  7655  genpassl  7672  genpassu  7673  nqprm  7690  nqprl  7699  nqpru  7700  ltsopr  7744  ltexprlemm  7748  ltexprlemloc  7755  suplocexprlemrl  7865  suplocexprlemloc  7869  axprecex  8028  axpre-ltirr  8030  sup3exmid  9065  2rexuz  9738  ioom  10440  nnwosdc  12475  4sqlemafi  12833  inffinp1  12915  omctfn  12929  nninfdclemp1  12936  ptex  13211  fngsum  13335  igsumvalx  13336  isbasis2g  14632  tgval2  14638  ntreq0  14719  bdcuni  16011  bj-axun2  16050