Definition df-rex 2918

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 2913	. 2 wff E. x e. A ph
5	2	cv 1482	. . . . 5 class x
6	5, 3	wcel 1990	. . . 4 wff x e. A
7	6, 1	wa 384	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1704	. 2 wff E. x ( x e. A /\ ph )
9	4, 8	wb 196	1 wff ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

This definition is referenced by:  ralnex  2992  ralnexOLD  2993  rexex  3002  rspe  3003  nfre1  3005  reximi2  3010  reximd2a  3013  reximdv2  3014  r19.23t  3021  rexbii2  3039  rexbida  3047  rexbidv2  3048  risset  3062  r19.41v  3089  r19.41  3090  reean  3106  rexeqf  3135  reu5  3159  rmo5  3162  cbvrexdva2  3176  rexv  3220  2gencl  3236  3gencl  3237  rspce  3304  ceqsrexv  3336  rexab  3369  rexab2  3373  rexrab2  3374  morex  3390  reu2  3394  reu6  3395  reu3  3396  2reuswap  3410  2reu5lem3  3415  2reu5  3416  ssrexf  3665  rexun  3793  reuss2  3907  reuun2  3910  reupick  3911  reupick3  3912  euelss  3914  reximdva0  3933  n0rex  3935  n0el  3940  rabn0OLD  3959  r19.2z  4060  r19.2zb  4061  rexsns  4217  exsnrex  4221  dfuni2  4438  eluni2  4440  elunirab  4448  iuncom4  4528  iunxiun  4608  intexrab  4823  elxp2OLD  5133  opeliunxp  5170  xpiundi  5173  xpiundir  5174  ssrelrn  5315  dmuni  5334  rnmpt  5371  elrnmpt1  5374  elres  5435  dfima2  5468  dfima3  5469  elima2  5472  dfco2a  5635  imaco  5640  elsnxp  5677  elsnxpOLD  5678  dffo4  6375  dffo5  6376  abrexco  6502  isomin  6587  zfrep6  7134  opabex3d  7145  opabex3  7146  abexssex  7149  abexex  7151  frxp  7287  dfrecs3  7469  rdglim2  7528  oarec  7642  oeeu  7683  mapsn  7899  mapsnen  8035  pssnn  8178  unblem2  8213  dffi2  8329  marypha2lem4  8344  marypha2  8345  zfregcl  8499  zfregclOLD  8501  axinf2  8537  zfinf2  8539  rankuni  8726  scott0  8749  cp  8754  bnd2  8756  infpwfien  8885  aceq1  8940  dfac5lem2  8947  dfac5lem3  8948  dfac2  8953  kmlem3  8974  kmlem6  8977  kmlem8  8979  kmlem14  8985  infmap2  9040  ackbij2  9065  cfub  9071  cfval2  9082  cflim3  9084  cfss  9087  cfslb  9088  isf32lem9  9183  zorn2lem6  9323  iundom2g  9362  winalim2  9518  grothprim  9656  genpass  9831  nqpr  9836  1idpr  9851  ltexprlem4  9861  ltexprlem5  9862  reclem2pr  9870  axrrecex  9984  dedekind  10200  sup2  10979  infm3  10982  nnunb  11288  2rexuz  11740  nnwos  11755  xrsupsslem  12137  xrinfmsslem  12138  ishashinf  13247  cshwsexa  13570  wwlktovfo  13701  ncoprmgcdne1b  15363  maxprmfct  15421  vdwapun  15678  vdwmc  15682  vdwmc2  15683  ram0  15726  imasleval  16201  mreexexlem2d  16305  dfiso2  16432  isssc  16480  drsdirfi  16938  dirge  17237  psgnunilem4  17917  odcau  18019  ablfac2  18488  lspprat  19153  lidlnz  19228  isbasis2g  20752  tgval2  20760  ntreq0  20881  neitr  20984  cmpfi  21211  is1stc2  21245  2ndcsb  21252  2ndcsep  21262  1stcelcls  21264  hausmapdom  21303  isfbas2  21639  fbssint  21642  isfil2  21660  elfg  21675  fgcl  21682  uffix2  21728  alexsubALTlem4  21854  lpbl  22308  metustexhalf  22361  metuel2  22370  restmetu  22375  bcthlem5  23125  upgrex  25987  uvtxa01vtx0  26297  uhgrvd00  26430  wlkpwwlkf1ouspgr  26765  wlknwwlksnsur  26776  wlkwwlksur  26783  wwlksnextsur  26795  frcond3  27133  frgr3vlem2  27138  3vfriswmgrlem  27141  frgrncvvdeqlem9  27171  ubthlem1  27726  axhcompl-zf  27855  isch3  28098  shne0i  28307  cnlnssadj  28939  2reuswap2  29328  rexunirn  29331  rmoxfrdOLD  29332  rmoxfrd  29333  abrexdomjm  29345  abrexexd  29347  1stpreimas  29483  fpwrelmapffslem  29507  ordtconnlem1  29970  ddemeas  30299  omssubaddlem  30361  omssubadd  30362  eulerpartlemgvv  30438  tgoldbachgt  30741  bnj168  30798  bnj956  30847  bnj1098  30854  bnj1143  30861  bnj1146  30862  bnj1185  30864  bnj1196  30865  bnj600  30989  bnj849  30995  bnj906  31000  bnj916  31003  bnj983  31021  bnj984  31022  bnj1083  31046  bnj1176  31073  bnj1186  31075  bnj1189  31077  bnj1228  31079  bnj1253  31085  bnj1398  31102  bnj1463  31123  bnj1312  31126  bnj1514  31131  erdszelem10  31182  ptpconn  31215  coep  31641  coepr  31642  dffr5  31643  dfpo2  31645  opelco3  31678  dfon2lem8  31695  brimg  32044  dfrecs2  32057  dfrdg4  32058  ellines  32259  neifg  32366  bj-rexvwv  32866  bj-rexcom4  32869  bj-snglc  32957  bj-snglss  32958  bj-rest10  33041  bj-restn0  33043  bj-restpw  33045  bj-rest0  33046  bj-restb  33047  bj-restuni  33050  bj-dfmpt2a  33071  bj-finsumval0  33147  rnmptsn  33182  f1omptsnlem  33183  mptsnunlem  33185  topdifinffinlem  33195  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlpssretop  33212  poimirlem30  33439  abrexdom  33525  prdstotbnd  33593  eldmqsres2  34052  exanres  34063  rncnvepres  34073  prtlem17  34161  prter2  34166  islshpat  34304  lsat0cv  34320  lshpsmreu  34396  atex  34692  islpln5  34821  islvol5  34865  pmapglb  35056  pmapglb2N  35057  pmapglb2xN  35058  elpaddn0  35086  pmapjat1  35139  polval2N  35192  osumcllem11N  35252  pexmidlem8N  35263  cdlemftr3  35853  dibelval3  36436  dibglbN  36455  dicelval3  36469  dihglbcpreN  36589  dihglb2  36631  dihjatcclem4  36710  mapdordlem2  36926  mapdrvallem2  36934  mapdpglem3  36964  hdmapglem7a  37219  rp-isfinite5  37863  rp-isfinite6  37864  relintabex  37887  elintima  37945  iunrelexpuztr  38011  cotrclrcl  38034  neik0pk1imk0  38345  ntrneineine0lem  38381  ntrneineine1lem  38382  ntrneiel2  38384  rexbidar  38650  onfrALTlem5  38757  onfrALTlem2  38761  onfrALTlem1  38763  onfrALTlem5VD  39121  onfrALTlem2VD  39125  onfrALTlem1VD  39126  chordthmALT  39169  rspcegf  39182  cncmpmax  39191  rfcnnnub  39195  inn0f  39242  nssrex  39260  eluni2f  39286  eliin2f  39287  suprnmpt  39355  founiiun0  39377  disjinfi  39380  mapsnd  39388  mapsnend  39391  fvelima2  39475  ssfiunibd  39523  infrpge  39567  fsumiunss  39807  islpcn  39871  lptre2pt  39872  stoweidlem14  40231  stoweidlem34  40251  stoweidlem35  40252  stoweidlem43  40260  stoweidlem44  40261  stoweidlem50  40267  stoweidlem54  40271  stoweidlem56  40273  stoweidlem59  40276  stoweidlem60  40277  fourier2  40444  qndenserrnbllem  40514  qndenserrn  40519  sge0rpcpnf  40638  hoidmvval0b  40804  hoiqssbllem3  40838  2rmoswap  41184  opeliun2xp  42111  setrec1lem3  42436