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

Theorem rgen 3153
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 3148 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1793 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789
This theorem depends on definitions:  df-bi 208  df-ral 3148
This theorem is referenced by:  ralel  3154  rgenw  3155  mprg  3157  mprgbir  3158  rgen2  3208  r19.21be  3215  rgen2a  3234  nrex  3274  rexlimiv  3285  rexlimi  3320  sbcth2  3871  r19.2zb  4444  ral0  4459  unimax  4872  mpteq1  5151  mpteq2ia  5154  reusv2lem4  5298  wfisg  6181  fnopab  6483  fmpti  6872  sorpssuni  7448  sorpssint  7449  onssmin  7500  tfis  7557  omssnlim  7582  finds  7596  finds2  7598  opabex3  7659  wfr3  7966  seqomlem2  8078  findcard3  8750  fifo  8885  fisupcl  8922  dfom3  9099  cantnfvalf  9117  rankf  9212  scottex  9303  cplem1  9307  harcard  9396  cardiun  9400  r0weon  9427  acnnum  9467  alephon  9484  alephsmo  9517  alephf1ALT  9518  alephfplem4  9522  dfac5lem4  9541  dfacacn  9556  kmlem1  9565  cflem  9657  cflecard  9664  cfsmolem  9681  fin23lem17  9749  hsmexlem4  9840  omina  10102  0tsk  10166  inar1  10186  wfgru  10227  reclem2pr  10459  nnssre  11631  nnsscn  11632  dfnn2  11640  dfnn3  11641  nnind  11645  nnsub  11670  dfuzi  12062  uzsupss  12329  cnref1o  12374  xrsupsslem  12690  xrinfmsslem  12691  xrsup0  12706  reltre  12723  rpltrp  12724  reltxrnmnf  12725  seqexw  13375  ser0f  13413  bccl  13672  hashkf  13682  hashbc  13801  wrdind  14074  sqrlem5  14596  sqrtf  14713  ackbijnn  15173  incexclem  15181  prodf1f  15238  eff2  15442  reeff1  15463  sqrt2irr  15592  prmind2  16019  3prm  16028  phisum  16117  pockthi  16233  infpn2  16239  prminf  16241  prmreclem2  16243  prmrec  16248  1arith  16253  1arith2  16254  vdwlem13  16319  ramz  16351  prmgap  16385  prmgaplcm  16386  prmgapprmo  16388  prmlem1a  16430  xpsff1o  16830  isacs1i  16918  dmaf  17299  cdaf  17300  coapm  17321  lublecllem  17588  pmtrdifel  18528  pmtrdifwrdel  18533  odf  18585  efgrelexlemb  18796  dprd2da  19084  mgpf  19229  prdscrngd  19283  cnfld1  20486  cnsubglem  20510  cnmsubglem  20524  nn0srg  20531  rge0srg  20532  pmatcoe1fsupp  21225  isbasis3g  21473  basdif0  21477  distop  21519  mretopd  21616  2ndcsep  21983  refref  22037  kqf  22271  fbssfi  22361  filconn  22407  prdstmdd  22647  ustfilxp  22736  prdsxmslem2  23054  qdensere  23293  recld2  23337  isclmi0  23617  iscvsi  23648  ovolf  23998  dyadmax  24114  dveflem  24491  mdegxrf  24577  fta1  24812  vieta1  24816  aalioulem2  24837  taylfval  24862  pilem2  24955  pilem3  24956  recosf1o  25032  divlogrlim  25131  logcn  25143  ressatans  25425  leibpi  25434  ftalem3  25566  chtub  25702  2sqlem6  25913  2sqlem10  25918  2sqreulem4  25944  chtppilim  25965  pntpbnd1  26076  pntlem3  26099  padicabvf  26121  axcontlem2  26665  nbgrnself  27055  vtxdginducedm1  27239  isgrpoi  28189  isvciOLD  28271  cnidOLD  28273  isnvi  28304  ipasslem8  28528  hilid  28852  hlimf  28928  shsspwh  28937  pjrni  29393  pjmf1  29407  df0op2  29443  dfiop2  29444  hoaddcomi  29463  hoaddassi  29467  hocadddiri  29470  hocsubdiri  29471  hoaddid1i  29477  ho0coi  29479  hoid1i  29480  hoid1ri  29481  honegsubi  29487  hoddii  29680  lnopunilem2  29702  elunop2  29704  lnophm  29710  imaelshi  29749  cnlnadjlem8  29765  pjnmopi  29839  pjsdii  29846  pjddii  29847  pjtoi  29870  chirred  30086  nnindf  30448  nn0min  30450  wrdt2ind  30541  ccfldsrarelvec  30942  esum2d  31238  dmvlsiga  31274  volmeas  31376  ddemeas  31381  sxbrsigalem3  31416  coinfliprv  31626  ballotlem7  31679  signsw0glem  31709  rpsqrtcn  31750  tgoldbachgt  31820  bnj580  32071  bnj1384  32188  bnj1497  32216  kur14lem9  32345  sat1el2xp  32510  msrf  32673  dfon2lem7  32918  frinsg  32971  bdayfo  33066  nodense  33080  fobigcup  33245  nn0prpwlem  33554  topmeet  33596  onsucsuccmpi  33675  taupilemrplb  34470  relowlssretop  34513  ptrecube  34759  poimirlem27  34786  heicant  34794  mblfinlem1  34796  volsupnfl  34804  dvtan  34809  itg2addnc  34813  indexa  34876  sstotbnd2  34920  heiborlem7  34963  atpsubN  36756  idldil  37117  cdleme50ldil  37551  mzpclall  39189  dgraaf  39612  arearect  39687  areaquad  39688  infordmin  39764  clsk1indlem2  40257  clsk1indlem4  40259  mnuunid  40478  mnurndlem1  40482  prmunb2  40508  radcnvrat  40511  unirnmapsn  41342  ssmapsn  41344  upbdrech  41437  supminfxr  41605  supminfxr2  41610  supminfxrrnmpt  41612  fsumiunss  41721  resincncf  42023  dmvolss  42136  volioof  42138  stoweidlem57  42208  wallispilem3  42218  stirlinglem13  42237  dirkertrigeqlem3  42251  fourierdlem62  42319  salexct  42483  salexct3  42491  salgencntex  42492  salgensscntex  42493  gsumge0cl  42519  0ome  42677  icoresmbl  42691  hoidmv1le  42742  smflimlem1  42913  smfpimbor1lem2  42940  smfliminflem  42970  ralndv1  43170  fmtno4prm  43569  31prm  43592  tgoldbach  43814  nn0mnd  43918  2zlidl  44037  2zrngagrp  44046  2zrngnmlid  44052  crhmsubc  44181  drhmsubc  44183  drngcat  44184  fldcat  44185  fldhmsubc  44187  crhmsubcALTV  44199  drhmsubcALTV  44201  drngcatALTV  44202  fldcatALTV  44203  fldhmsubcALTV  44205  zlmodzxznm  44384  ldepsnlinc  44395  nn0sumshdiglem2  44514  rrx2xpref1o  44537  onsetrec  44642
  Copyright terms: Public domain W3C validator