Definition df-rex 2514

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 2509	. 2 wff E. x e. A ph
5	2	cv 1394	. . . . 5 class x
6	5, 3	wcel 2200	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1538	. 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  2518  rexnalim  2519  dfrex2dc  2521  rexbida  2525  rexbidv2  2533  rexbid2  2535  rexbii2  2541  r2exf  2548  risset  2558  nfrexdxy  2564  nfrexdya  2566  nfre1  2573  rexex  2576  rspe  2579  rsp2e  2581  rexim  2624  reximi2  2626  reximdv2  2629  r19.23t  2638  r19.41  2686  r19.43  2689  reean  2700  rexeqf  2725  reu5  2749  rmo5  2752  cbvrexfw  2755  cbvrexf  2757  cbvrexvw  2770  cbvrexdva2  2773  rexv  2819  2gencl  2834  3gencl  2835  rspce  2903  rspcimedv  2910  ceqsrexv  2934  rexab  2966  rexab2  2970  rexrab2  2971  morex  2988  reu2  2992  reu6  2993  reu3  2994  2reuswapdc  3008  2rmorex  3010  cbvrexcsf  3189  ssrexf  3287  rexun  3385  reuss2  3485  reuun2  3488  reupick  3489  reupick3  3490  reximdva0m  3508  rabn0r  3519  rabn0m  3520  r19.2m  3579  r19.2mOLD  3580  r19.9rmv  3584  rexm  3592  rexsns  3706  exsnrex  3709  dfuni2  3893  eluni2  3895  elunirab  3904  iuncom4  3975  iunxiun  4050  intexrabim  4241  bnd2  4261  rexxfrd  4558  elxp2  4741  opeliunxp  4779  xpiundi  4782  xpiundir  4783  rexiunxp  4870  ssrelrn  4920  dmuni  4939  rnmpt  4978  elrnmpt1  4981  elres  5047  dfima2  5076  dfima3  5077  elima2  5080  dfco2a  5235  imaco  5240  imadiflem  5406  imadif  5407  imainlem  5408  imain  5409  funimaexglem  5410  fvelrnb  5689  rexrnmpt  5786  dffo4  5791  dffo5  5792  abrexco  5895  opabex3d  6278  opabex3  6279  abexssex  6282  abexex  6283  ecexr  6702  mapsn  6854  mapsnen  6981  fimax2gtri  7084  ctssdccl  7301  ltexnqq  7618  subhalfnqq  7624  ltbtwnnq  7626  nqnq0  7651  prnmaxl  7698  prnminu  7699  prarloc  7713  genpdflem  7717  genpassl  7734  genpassu  7735  nqprm  7752  nqprl  7761  nqpru  7762  ltsopr  7806  ltexprlemm  7810  ltexprlemloc  7817  suplocexprlemrl  7927  suplocexprlemloc  7931  axprecex  8090  axpre-ltirr  8092  sup3exmid  9127  2rexuz  9806  ioom  10510  nnwosdc  12600  4sqlemafi  12958  inffinp1  13040  omctfn  13054  nninfdclemp1  13061  ptex  13337  fngsum  13461  igsumvalx  13462  isbasis2g  14759  tgval2  14765  ntreq0  14846  bdcuni  16407  bj-axun2  16446