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

Theorem rgenw 2775
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 11 . 2  |-  ( x  e.  A  ->  ph )
32rgen 2773 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   A.wral 2707
This theorem is referenced by:  rgen2w  2776  reuun1  3625  riinrab  4168  0disj  4207  iinexg  4362  epse  4567  xpiindi  5012  eliunxp  5014  opeliunxp2  5015  elrnmpti  5123  fnmpti  5575  eqfnfv  5829  eufnfv  5974  iunex  5993  mpt2eq12  6136  mpt2ex  6427  porpss  6528  onnseq  6608  ixpssmap  7098  boxcutc  7107  nneneq  7292  finsschain  7415  dfom3  7604  cantnfdm  7621  cantnf  7651  rankuni2b  7781  rankval4  7795  alephf1  7968  dfac4  8005  dfacacn  8023  infmap2  8100  cfeq0  8138  fin23lem28  8222  axdc2lem  8330  axcclem  8339  ac6  8362  iundom  8419  konigthlem  8445  iunctb  8451  tskmid  8717  supmul1  9975  supmullem2  9977  supmul  9978  uzf  10493  seqof  11382  hashbclem  11703  wrdexg  11741  rlimclim1  12341  fsumcom2  12560  ackbijnn  12609  sumhash  13267  ramcl  13399  prdsval  13680  prdsbas  13682  prdshom  13691  imasplusg  13745  imasmulr  13746  imasvsca  13748  imasaddfnlem  13755  imasvscafn  13764  isfunc  14063  wunfunc  14098  isnat  14146  natffn  14148  wunnat  14155  fucsect  14171  setcepi  14245  spwpr4c  14666  dfod2  15202  ghmcyg  15507  gsum2d2lem  15549  gsum2d2  15550  gsumcom2  15551  dmdprd  15561  dprdval  15563  dprdf11  15583  dprd2d2  15604  dpjeq  15619  pgpfac1lem2  15635  pgpfac1lem3  15637  pgpfac1lem4  15638  00lsp  16059  ocv0  16906  tgidm  17047  pptbas  17074  tgrest  17225  iscnp2  17305  ist1-3  17415  discmp  17463  1stcfb  17510  lly1stc  17561  disllycmp  17563  dis1stc  17564  txbas  17601  ptbasfi  17615  ptpjopn  17646  dfac14  17652  ptrescn  17673  xkoptsub  17688  fclsval  18042  ptcmplem2  18086  ptcmplem3  18087  cnextrel  18096  tsmsfbas  18159  ustuqtop  18278  prdsxmetlem  18400  ressprdsds  18403  prdsxmslem2  18561  zcld  18846  xrge0tsms  18867  metdsf  18880  metdsge  18881  minveclem1  19327  minveclem3b  19331  minveclem6  19337  uniioombllem4  19480  uniioombllem6  19482  ismbf3d  19548  i1f1lem  19583  reldv  19759  ellimc2  19766  limcflf  19770  limciun  19783  dvfval  19786  dvrec  19843  dvlipcn  19880  mdegle0  20002  ply1nzb  20047  quotlem  20219  taylfval  20277  ulmdvlem1  20318  ulmdvlem2  20319  ulmdvlem3  20320  psercn  20344  sqff1o  20967  lgsquadlem2  21141  cusgrasizeindslem2  21485  grpoidval  21806  grpoidinv2  21808  grpoinv  21817  minvecolem1  22378  minvecolem5  22385  minvecolem6  22386  adjbdln  23588  rexdiv  24174  xrge0tsmsd  24225  esumnul  24445  esum0  24446  hasheuni  24477  measvuni  24570  measdivcstOLD  24580  probfinmeasbOLD  24688  0rrv  24711  subfacf  24863  subfacp1lem6  24873  cvmsss2  24963  cvmliftlem1  24974  fprodcom2  25310  supaddc  26239  supadd  26240  cnambfre  26257  comppfsc  26389  upixp  26433  0totbnd  26484  prdsbnd  26504  prdstotbnd  26505  cntotbnd  26507  rrnequiv  26546  0dioph  26839  vdioph  26840  rmxyelqirr  26975  pw2f1ocnv  27110  phisum  27497  bnj226  29103  bnj98  29240  bnj517  29258  bnj893  29301  bnj1137  29366  cdlemefrs32fva  31199  cdlemkid5  31734  cdlemk56  31770  dihf11lem  32066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556
This theorem depends on definitions:  df-bi 179  df-ral 2712
  Copyright terms: Public domain W3C validator