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

Theorem rgen 2905
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 2900 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1716 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712
This theorem depends on definitions:  df-bi 195  df-ral 2900
This theorem is referenced by:  ralel  2906  rgenw  2907  mprg  2909  mprgbir  2910  r19.21be  2916  rgen2  2957  rgen2a  2959  nrex  2982  rexlimi  3005  rexlimiv  3008  sbcth2  3488  r19.2zb  4012  ral0  4027  unimax  4403  mpteq1  4659  mpteq2ia  4662  reusv2lem4  4793  wfisg  5618  fnopab  5917  fmpti  6276  sorpssuni  6821  sorpssint  6822  onssmin  6866  tfis  6923  omssnlim  6948  finds  6961  finds2  6963  opabex3  7015  wfr3  7299  seqomlem2  7410  findcard3  8065  fifo  8198  fisupcl  8235  dfom3  8404  cantnfvalf  8422  rankf  8517  scottex  8608  cplem1  8612  harcard  8664  cardiun  8668  r0weon  8695  acnnum  8735  alephon  8752  alephsmo  8785  alephf1ALT  8786  alephfplem4  8790  dfac5lem4  8809  dfacacn  8823  kmlem1  8832  cflem  8928  cflecard  8935  cfsmolem  8952  fin23lem17  9020  hsmexlem4  9111  omina  9369  0tsk  9433  inar1  9453  wfgru  9494  reclem2pr  9726  nnssre  10871  dfnn2  10880  dfnn3  10881  nnind  10885  nnsub  10906  dfuzi  11300  uzsupss  11612  cnref1o  11659  xrsupsslem  11965  xrinfmsslem  11966  xrsup0  11981  reltre  11997  rpltrp  11998  reltxrnmnf  11999  ser0f  12671  bccl  12926  hashkf  12936  hashbc  13046  wrdind  13274  sqrlem5  13781  rexuz3  13882  sqrtf  13897  ackbijnn  14345  incexclem  14353  prodf1f  14409  eff2  14614  reeff1  14635  sqrt2irr  14763  prmind2  15182  3prm  15190  phisum  15279  pockthi  15395  infpn2  15401  prminf  15403  prmreclem2  15405  prmrec  15410  1arith  15415  1arith2  15416  vdwlem13  15481  ramz  15513  prmgap  15547  prmgaplcm  15548  prmgapprmo  15550  prmlem1a  15597  xpsff1o  15997  isacs1i  16087  dmaf  16468  cdaf  16469  coapm  16490  lublecllem  16757  pmtrdifel  17669  pmtrdifwrdel  17674  odf  17725  efgrelexlemb  17932  dprd2da  18210  mgpf  18328  prdscrngd  18382  cnfld1  19536  cnsubglem  19560  cnmsubglem  19574  nn0srg  19581  rge0srg  19582  pmatcoe1fsupp  20267  isbasis3g  20506  basdif0  20510  distop  20552  mretopd  20648  2ndcsep  21014  refref  21068  kqf  21302  fbssfi  21393  filcon  21439  prdstmdd  21679  ustfilxp  21768  prdsxmslem2  22085  qdensere  22315  recld2  22357  isclmi0  22637  iscvsi  22666  ovolf  22974  dyadmax  23089  dveflem  23463  mdegxrf  23549  fta1  23784  vieta1  23788  aalioulem2  23809  taylfval  23834  pilem2  23927  pilem3  23928  recosf1o  24002  divlogrlim  24098  logcn  24110  ressatans  24378  leibpi  24386  ftalem3  24518  chtub  24654  2sqlem6  24865  2sqlem10  24870  chtppilim  24881  pntpbnd1  24992  pntlem3  25015  padicabvf  25037  axcontlem2  25563  isgrpoi  26502  isvciOLD  26603  cnidOLD  26605  isnvi  26636  ipasslem8  26882  hilid  27208  hlimf  27284  shsspwh  27293  pjrni  27751  pjmf1  27765  df0op2  27801  dfiop2  27802  hoaddcomi  27821  hoaddassi  27825  hocadddiri  27828  hocsubdiri  27829  hoaddid1i  27835  ho0coi  27837  hoid1i  27838  hoid1ri  27839  honegsubi  27845  hoddii  28038  lnopunilem2  28060  elunop2  28062  lnophm  28068  imaelshi  28107  cnlnadjlem8  28123  pjnmopi  28197  pjsdii  28204  pjddii  28205  pjtoi  28228  chirred  28444  nnindf  28758  nn0min  28760  esum2d  29288  dmvlsiga  29325  volmeas  29427  ddemeas  29432  sxbrsigalem3  29467  coinfliprv  29677  ballotlem7  29730  signsw0glem  29762  bnj580  30043  bnj1384  30160  bnj1497  30188  kur14lem9  30256  msrf  30499  dfon2lem7  30744  frinsg  30792  bdayfo  30880  nodense  30894  fobigcup  30983  nn0prpwlem  31293  topmeet  31335  onsucsuccmpi  31418  taupilemrplb  32139  relowlssretop  32183  ptrecube  32375  poimirlem27  32402  heicant  32410  mblfinlem1  32412  volsupnfl  32420  dvtan  32426  itg2addnc  32430  indexa  32494  sstotbnd2  32539  heiborlem7  32582  atpsubN  33853  idldil  34214  cdleme50ldil  34650  mzpclall  36104  dgraaf  36532  arearect  36616  areaquad  36617  clsk1indlem2  37156  clsk1indlem4  37158  prmunb2  37328  radcnvrat  37331  ssrab2f  38127  unirnmapsn  38197  ssmapsn  38199  upbdrech  38256  fsumiunss  38439  resincncf  38557  dmvolss  38675  volioof  38677  stoweidlem57  38747  wallispilem3  38757  stirlinglem13  38776  dirkertrigeqlem3  38790  fourierdlem62  38858  salexct  39025  salexct3  39033  salgencntex  39034  salgensscntex  39035  gsumge0cl  39061  0ome  39216  icoresmbl  39230  hoidmv1le  39281  smflimlem1  39454  smfpimbor1lem2  39481  fmtno4prm  39823  31prm  39848  tgoldbach  40030  tgoldbachOLD  40037  nbgrnself  40578  2zlidl  41719  2zrngagrp  41728  2zrngnmlid  41734  crhmsubc  41865  drhmsubc  41867  drngcat  41868  fldcat  41869  fldhmsubc  41871  crhmsubcALTV  41884  drhmsubcALTV  41886  drngcatALTV  41887  fldcatALTV  41888  fldhmsubcALTV  41890  zlmodzxznm  42075  ldepsnlinc  42086  nn0sumshdiglem2  42209
  Copyright terms: Public domain W3C validator