Definition df-rex 2449

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 2444	. 2 wff E. x e. A ph
5	2	cv 1342	. . . . 5 class x
6	5, 3	wcel 2136	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1480	. 2 wff E. x ( x e. A /\ ph )
9	4, 8	wb 104	1 wff ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

This definition is referenced by:  ralnex  2453  rexnalim  2454  dfrex2dc  2456  rexbida  2460  rexbidv2  2468  rexbid2  2470  rexbii2  2476  r2exf  2483  risset  2493  nfrexdxy  2499  nfrexdya  2501  nfre1  2508  rexex  2511  rspe  2514  rsp2e  2516  rexim  2559  reximi2  2561  reximdv2  2564  r19.23t  2572  r19.41  2620  r19.43  2623  reean  2633  rexeqf  2657  reu5  2677  rmo5  2680  cbvrexfw  2683  cbvrexf  2685  cbvrexvw  2696  cbvrexdva2  2699  rexv  2743  2gencl  2758  3gencl  2759  rspce  2824  rspcimedv  2831  ceqsrexv  2855  rexab  2887  rexab2  2891  rexrab2  2892  morex  2909  reu2  2913  reu6  2914  reu3  2915  2reuswapdc  2929  2rmorex  2931  cbvrexcsf  3107  ssrexf  3203  rexun  3301  reuss2  3401  reuun2  3404  reupick  3405  reupick3  3406  reximdva0m  3423  rabn0r  3434  rabn0m  3435  r19.2m  3494  r19.2mOLD  3495  r19.9rmv  3499  rexm  3507  rexsns  3614  exsnrex  3617  dfuni2  3790  eluni2  3792  elunirab  3801  iuncom4  3872  iunxiun  3946  intexrabim  4131  bnd2  4151  rexxfrd  4440  elxp2  4621  opeliunxp  4658  xpiundi  4661  xpiundir  4662  rexiunxp  4745  dmuni  4813  rnmpt  4851  elrnmpt1  4854  elres  4919  dfima2  4947  dfima3  4948  elima2  4951  dfco2a  5103  imaco  5108  imadiflem  5266  imadif  5267  imainlem  5268  imain  5269  funimaexglem  5270  fvelrnb  5533  rexrnmpt  5627  dffo4  5632  dffo5  5633  abrexco  5726  opabex3d  6086  opabex3  6087  abexssex  6090  abexex  6091  ecexr  6502  mapsn  6652  mapsnen  6773  fimax2gtri  6863  ctssdccl  7072  ltexnqq  7345  subhalfnqq  7351  ltbtwnnq  7353  nqnq0  7378  prnmaxl  7425  prnminu  7426  prarloc  7440  genpdflem  7444  genpassl  7461  genpassu  7462  nqprm  7479  nqprl  7488  nqpru  7489  ltsopr  7533  ltexprlemm  7537  ltexprlemloc  7544  suplocexprlemrl  7654  suplocexprlemloc  7658  axprecex  7817  axpre-ltirr  7819  sup3exmid  8848  2rexuz  9516  ioom  10192  nnwosdc  11968  inffinp1  12358  omctfn  12372  nninfdclemp1  12379  isbasis2g  12643  tgval2  12651  ntreq0  12732  bdcuni  13718  bj-axun2  13757