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

Theorem rgen 2817
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rgen.1
Assertion
Ref Expression
rgen

Proof of Theorem rgen
StepHypRef Expression
1 df-ral 2812 . 2
2 rgen.1 . 2
31, 2mpgbir 1622 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807
This theorem is referenced by:  rgenw  2818  mprg  2820  mprgbir  2821  r19.21be  2828  rgen2  2882  rgen2a  2884  rgen2aOLD  2885  nrex  2912  rexlimi  2939  rexlimiv  2943  sbcth2  3422  reuss  3778  r19.2zb  3919  ral0  3934  unimax  4285  mpteq1  4532  mpteq2ia  4534  reusv2lem4  4656  fnopab  5710  fmpti  6054  sorpssuni  6589  sorpssint  6590  onssmin  6632  tfis  6689  omssnlim  6714  finds  6726  finds2  6728  opabex3  6779  seqomlem2  7135  findcard3  7783  fifo  7912  fisupcl  7948  dfom3  8085  cantnfvalf  8105  rankf  8233  scottex  8324  cplem1  8328  harcard  8380  cardiun  8384  r0weon  8411  acnnum  8454  alephon  8471  alephsmo  8504  alephf1ALT  8505  alephfplem4  8509  dfac5lem4  8528  dfacacn  8542  kmlem1  8551  cflem  8647  cflecard  8654  cfsmolem  8671  fin23lem17  8739  hsmexlem4  8830  omina  9090  0tsk  9154  inar1  9174  wfgru  9215  reclem2pr  9447  nnssre  10565  dfnn2  10574  dfnn3  10575  nnind  10579  nnsub  10599  dfuzi  10978  uzinfmi  11190  uzsupss  11203  cnref1o  11244  xrsupsslem  11527  xrinfmsslem  11528  xrsup0  11544  ser0f  12160  bccl  12400  hashkf  12407  hashbc  12502  wrdind  12702  sqrlem5  13080  rexuz3  13181  sqrtf  13196  ackbijnn  13640  incexclem  13648  prodf1f  13701  eff2  13834  reeff1  13855  sqrt2irr  13982  prmind2  14228  3prm  14234  pockthi  14425  infpn2  14431  prminf  14433  prmreclem2  14435  prmrec  14440  1arith  14445  1arith2  14446  vdwlem13  14511  ramz  14543  prmlem1a  14592  xpsff1o  14965  isacs1i  15054  dmaf  15376  cdaf  15377  coapm  15398  lublecllem  15618  pmtrdifel  16505  pmtrdifwrdel  16510  odf  16561  efgrelexlemb  16768  dprd2da  17091  mgpf  17210  prdscrngd  17262  cnfld1  18443  cnsubglem  18467  cnmsubglem  18480  nn0srg  18486  rge0srg  18487  pmatcoe1fsupp  19202  isbasis3g  19450  basdif0  19454  distop  19497  mretopd  19593  2ndcsep  19960  refref  20014  kqf  20248  fbssfi  20338  filcon  20384  prdstmdd  20622  ustfilxp  20715  prdsxmslem2  21032  qdensere  21277  recld2  21319  ovolf  21893  dyadmax  22007  dveflem  22380  mdegxrf  22468  fta1  22704  vieta1  22708  aalioulem2  22729  taylfval  22754  pilem2  22847  pilem3  22848  recosf1o  22922  divlogrlim  23016  logcn  23028  ressatans  23265  leibpi  23273  ftalem3  23348  chtub  23487  2sqlem6  23644  2sqlem10  23649  chtppilim  23660  pntpbnd1  23771  pntlem3  23794  padicabvf  23816  axcontlem2  24268  isgrpoi  25200  cnid  25353  mulid  25358  cnrngo  25405  isvci  25475  isnvi  25506  ipasslem8  25752  hilid  26078  hlimf  26155  shsspwh  26164  pjrni  26620  pjmf1  26634  df0op2  26671  dfiop2  26672  hoaddcomi  26691  hoaddassi  26695  hocadddiri  26698  hocsubdiri  26699  hoaddid1i  26705  ho0coi  26707  hoid1i  26708  hoid1ri  26709  honegsubi  26715  hoddii  26908  lnopunilem2  26930  elunop2  26932  lnophm  26938  imaelshi  26977  cnlnadjlem8  26993  pjnmopi  27067  pjsdii  27074  pjddii  27075  pjtoi  27098  chirred  27314  nnindf  27610  nn0min  27611  dmvlsiga  28129  volmeas  28203  ddemeas  28208  sxbrsigalem3  28243  coinfliprv  28421  ballotlem7  28474  signsw0glem  28510  kur14lem9  28658  msrf  28902  dfon2lem7  29221  epsetlike  29274  wfisg  29289  frinsg  29325  wfr3  29361  tfrALTlem  29362  bdayfo  29435  nodense  29449  fobigcup  29550  onsucsuccmpi  29908  heicant  30049  mblfinlem1  30051  volsupnfl  30059  dvtan  30065  itg2addnc  30069  nn0prpwlem  30140  topmeet  30182  indexa  30224  sstotbnd2  30270  heiborlem7  30313  mzpclall  30659  dgraaf  31096  phisum  31159  arearect  31183  areaquad  31184  prmunb2  31191  radcnvrat  31195  upbdrech  31505  resincncf  31677  stoweidlem57  31839  wallispilem3  31849  stirlinglem13  31868  dirkertrigeqlem3  31882  fourierdlem62  31951  2zlidl  32740  2zrngagrp  32749  2zrngnmlid  32755  crhmsubc  32886  drhmsubc  32888  drngcat  32889  fldcat  32890  fldhmsubc  32892  crhmsubcOLD  32905  drhmsubcOLD  32907  drngcatOLD  32908  fldcatOLD  32909  fldhmsubcOLD  32911  zlmodzxznm  33098  ldepsnlinc  33109  bnj580  33971  bnj1384  34088  bnj1497  34116  atpsubN  35477  idldil  35838  cdleme50ldil  36274  taupilemrplb  37695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator