MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgenw Unicode version

Theorem rgenw 2610
Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rgenw.1  |-  ph
Assertion
Ref Expression
rgenw  |-  A. x  e.  A  ph

Proof of Theorem rgenw
StepHypRef Expression
1 rgenw.1 . . 3  |-  ph
21a1i 10 . 2  |-  ( x  e.  A  ->  ph )
32rgen 2608 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   A.wral 2543
This theorem is referenced by:  rgen2w  2611  reuun1  3450  riinrab  3977  0disj  4016  iinexg  4171  epse  4376  xpiindi  4821  eliunxp  4823  opeliunxp2  4824  elrnmpti  4930  fnmpti  5372  eqfnfv  5622  eufnfv  5752  iunex  5770  mpt2eq12  5908  mpt2ex  6198  relmpt2opab  6201  porpss  6281  onnseq  6361  ixpssmap  6850  boxcutc  6859  nneneq  7044  finsschain  7162  dfom3  7348  cantnfdm  7365  cantnf  7395  rankuni2b  7525  rankval4  7539  alephf1  7712  dfac4  7749  dfacacn  7767  infmap2  7844  cfeq0  7882  fin23lem28  7966  axdc2lem  8074  axcclem  8083  ac6  8107  iundom  8164  konigthlem  8190  iunctb  8196  wuncid  8365  tskmid  8462  supmul1  9719  supmullem2  9721  supmul  9722  uzf  10233  seqof  11103  hashbclem  11390  wrdexg  11425  rlimclim1  12019  fsumcom2  12237  ackbijnn  12286  sumhash  12944  ramcl  13076  prdsval  13355  prdsbas  13357  prdshom  13366  imasplusg  13420  imasmulr  13421  imasvsca  13423  imasaddfnlem  13430  imasvscafn  13439  isfunc  13738  wunfunc  13773  isnat  13821  natffn  13823  wunnat  13830  fucsect  13846  setcepi  13920  spwpr4c  14341  dfod2  14877  ghmcyg  15182  gsum2d2lem  15224  gsum2d2  15225  gsumcom2  15226  dmdprd  15236  dprdval  15238  dprdf11  15258  dprd2d2  15279  dpjeq  15294  pgpfac1lem2  15310  pgpfac1lem3  15312  pgpfac1lem4  15313  00lsp  15738  ocv0  16577  tgidm  16718  pptbas  16745  tgrest  16890  iscnp2  16969  ist1-3  17077  discmp  17125  1stcfb  17171  lly1stc  17222  disllycmp  17224  dis1stc  17225  txbas  17262  ptbasfi  17276  ptpjopn  17306  dfac14  17312  ptrescn  17333  xkoptsub  17348  fclsval  17703  ptcmplem2  17747  ptcmplem3  17748  tsmsfbas  17810  prdsxmetlem  17932  ressprdsds  17935  prdsxmslem2  18075  zcld  18319  xrge0tsms  18339  metdsf  18352  metdsge  18353  minveclem1  18788  minveclem3b  18792  minveclem6  18798  uniioombllem4  18941  uniioombllem6  18943  ismbf3d  19009  i1f1lem  19044  reldv  19220  ellimc2  19227  limcflf  19231  limciun  19244  dvfval  19247  dvrec  19304  dvlipcn  19341  mdegle0  19463  ply1nzb  19508  quotlem  19680  taylfval  19738  ulmdvlem1  19777  ulmdvlem2  19778  ulmdvlem3  19779  psercn  19802  sqff1o  20420  lgsquadlem2  20594  grpoidval  20883  grpoidinv2  20885  grpoinv  20894  minvecolem1  21453  minvecolem5  21460  minvecolem6  21461  adjbdln  22663  rexdiv  23109  xppreima2  23212  feqmptdf  23228  xrge0mulc1cn  23323  xrge0tsmsd  23382  esumnul  23427  esum0  23428  hasheuni  23453  ofcfn  23461  measvuni  23542  measdivcstOLD  23551  measdivcst  23552  probfinmeasbOLD  23631  0rrv  23654  subfacf  23706  subfacp1lem6  23716  cvmsss2  23805  cvmliftlem1  23816  trooo  25394  trinv  25395  ltrooo  25404  rltrooo  25415  usptoplem  25546  istopx  25547  prcnt  25551  isKleene  25988  comppfsc  26307  upixp  26403  0totbnd  26497  prdsbnd  26517  prdstotbnd  26518  cntotbnd  26520  rrnequiv  26559  0dioph  26858  vdioph  26859  rmxyelqirr  26995  pw2f1ocnv  27130  phisum  27518  bnj226  28762  bnj98  28899  bnj517  28917  bnj893  28960  bnj1137  29025  cdlemefrs32fva  30589  cdlemkid5  31124  cdlemk56  31160  dihf11lem  31456
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator