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

Theorem rgenw 2623
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 2621 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   A.wral 2556
This theorem is referenced by:  rgen2w  2624  reuun1  3463  riinrab  3993  0disj  4032  iinexg  4187  epse  4392  xpiindi  4837  eliunxp  4839  opeliunxp2  4840  elrnmpti  4946  fnmpti  5388  eqfnfv  5638  eufnfv  5768  iunex  5786  mpt2eq12  5924  mpt2ex  6214  relmpt2opab  6217  porpss  6297  onnseq  6377  ixpssmap  6866  boxcutc  6875  nneneq  7060  finsschain  7178  dfom3  7364  cantnfdm  7381  cantnf  7411  rankuni2b  7541  rankval4  7555  alephf1  7728  dfac4  7765  dfacacn  7783  infmap2  7860  cfeq0  7898  fin23lem28  7982  axdc2lem  8090  axcclem  8099  ac6  8123  iundom  8180  konigthlem  8206  iunctb  8212  wuncid  8381  tskmid  8478  supmul1  9735  supmullem2  9737  supmul  9738  uzf  10249  seqof  11119  hashbclem  11406  wrdexg  11441  rlimclim1  12035  fsumcom2  12253  ackbijnn  12302  sumhash  12960  ramcl  13092  prdsval  13371  prdsbas  13373  prdshom  13382  imasplusg  13436  imasmulr  13437  imasvsca  13439  imasaddfnlem  13446  imasvscafn  13455  isfunc  13754  wunfunc  13789  isnat  13837  natffn  13839  wunnat  13846  fucsect  13862  setcepi  13936  spwpr4c  14357  dfod2  14893  ghmcyg  15198  gsum2d2lem  15240  gsum2d2  15241  gsumcom2  15242  dmdprd  15252  dprdval  15254  dprdf11  15274  dprd2d2  15295  dpjeq  15310  pgpfac1lem2  15326  pgpfac1lem3  15328  pgpfac1lem4  15329  00lsp  15754  ocv0  16593  tgidm  16734  pptbas  16761  tgrest  16906  iscnp2  16985  ist1-3  17093  discmp  17141  1stcfb  17187  lly1stc  17238  disllycmp  17240  dis1stc  17241  txbas  17278  ptbasfi  17292  ptpjopn  17322  dfac14  17328  ptrescn  17349  xkoptsub  17364  fclsval  17719  ptcmplem2  17763  ptcmplem3  17764  tsmsfbas  17826  prdsxmetlem  17948  ressprdsds  17951  prdsxmslem2  18091  zcld  18335  xrge0tsms  18355  metdsf  18368  metdsge  18369  minveclem1  18804  minveclem3b  18808  minveclem6  18814  uniioombllem4  18957  uniioombllem6  18959  ismbf3d  19025  i1f1lem  19060  reldv  19236  ellimc2  19243  limcflf  19247  limciun  19260  dvfval  19263  dvrec  19320  dvlipcn  19357  mdegle0  19479  ply1nzb  19524  quotlem  19696  taylfval  19754  ulmdvlem1  19793  ulmdvlem2  19794  ulmdvlem3  19795  psercn  19818  sqff1o  20436  lgsquadlem2  20610  grpoidval  20899  grpoidinv2  20901  grpoinv  20910  minvecolem1  21469  minvecolem5  21476  minvecolem6  21477  adjbdln  22679  rexdiv  23125  xppreima2  23227  feqmptdf  23243  xrge0mulc1cn  23338  xrge0tsmsd  23397  esumnul  23442  esum0  23443  hasheuni  23468  ofcfn  23476  measvuni  23557  measdivcstOLD  23566  measdivcst  23567  probfinmeasbOLD  23646  0rrv  23669  subfacf  23721  subfacp1lem6  23731  cvmsss2  23820  cvmliftlem1  23831  supaddc  24995  supadd  24996  trooo  25497  trinv  25498  ltrooo  25507  rltrooo  25518  usptoplem  25649  istopx  25650  prcnt  25654  isKleene  26091  comppfsc  26410  upixp  26506  0totbnd  26600  prdsbnd  26620  prdstotbnd  26621  cntotbnd  26623  rrnequiv  26662  0dioph  26961  vdioph  26962  rmxyelqirr  27098  pw2f1ocnv  27233  phisum  27621  bnj226  29078  bnj98  29215  bnj517  29233  bnj893  29276  bnj1137  29341  cdlemefrs32fva  31211  cdlemkid5  31746  cdlemk56  31782  dihf11lem  32078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator