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

Theorem rgen 3110
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 3101 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1881 1 𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877
This theorem depends on definitions:  df-bi 198  df-ral 3101
This theorem is referenced by:  ralel  3111  rgenw  3112  mprg  3114  mprgbir  3115  r19.21be  3121  rgen2  3163  rgen2a  3165  nrex  3187  rexlimi  3212  rexlimiv  3215  sbcth2  3718  r19.2zb  4256  ral0  4271  unimax  4667  mpteq1  4931  mpteq2ia  4934  reusv2lem4  5070  wfisg  5928  fnopab  6225  fmpti  6600  sorpssuni  7172  sorpssint  7173  onssmin  7223  tfis  7280  omssnlim  7305  finds  7318  finds2  7320  opabex3  7372  wfr3  7667  seqomlem2  7778  findcard3  8438  fifo  8573  fisupcl  8610  dfom3  8787  cantnfvalf  8805  rankf  8900  scottex  8991  cplem1  8995  harcard  9083  cardiun  9087  r0weon  9114  acnnum  9154  alephon  9171  alephsmo  9204  alephf1ALT  9205  alephfplem4  9209  dfac5lem4  9228  dfacacn  9244  kmlem1  9253  cflem  9349  cflecard  9356  cfsmolem  9373  fin23lem17  9441  hsmexlem4  9532  omina  9794  0tsk  9858  inar1  9878  wfgru  9919  reclem2pr  10151  nnssre  11305  dfnn2  11314  dfnn3  11315  nnind  11319  nnsub  11341  dfuzi  11730  uzsupss  11995  cnref1o  12037  xrsupsslem  12351  xrinfmsslem  12352  xrsup0  12367  reltre  12384  rpltrp  12385  reltxrnmnf  12386  ser0f  13073  bccl  13325  hashkf  13335  hashbc  13450  wrdind  13696  sqrlem5  14206  rexuz3  14307  sqrtf  14322  ackbijnn  14778  incexclem  14786  prodf1f  14841  eff2  15045  reeff1  15066  sqrt2irr  15195  prmind2  15612  3prm  15620  phisum  15708  pockthi  15824  infpn2  15830  prminf  15832  prmreclem2  15834  prmrec  15839  1arith  15844  1arith2  15845  vdwlem13  15910  ramz  15942  prmgap  15976  prmgaplcm  15977  prmgapprmo  15979  prmlem1a  16021  xpsff1o  16429  isacs1i  16518  dmaf  16899  cdaf  16900  coapm  16921  lublecllem  17189  pmtrdifel  18097  pmtrdifwrdel  18102  odf  18153  efgrelexlemb  18360  dprd2da  18639  mgpf  18757  prdscrngd  18811  cnfld1  19975  cnsubglem  19999  cnmsubglem  20013  nn0srg  20020  rge0srg  20021  pmatcoe1fsupp  20716  isbasis3g  20964  basdif0  20968  distop  21010  mretopd  21107  2ndcsep  21473  refref  21527  kqf  21761  fbssfi  21851  filconn  21897  prdstmdd  22137  ustfilxp  22226  prdsxmslem2  22544  qdensere  22783  recld2  22827  isclmi0  23107  iscvsi  23138  ovolf  23462  dyadmax  23578  dveflem  23955  mdegxrf  24041  fta1  24276  vieta1  24280  aalioulem2  24301  taylfval  24326  pilem2  24419  pilem3  24420  pilem3OLD  24421  recosf1o  24495  divlogrlim  24594  logcn  24606  ressatans  24874  leibpi  24882  ftalem3  25014  chtub  25150  2sqlem6  25361  2sqlem10  25366  chtppilim  25377  pntpbnd1  25488  pntlem3  25511  padicabvf  25533  axcontlem2  26058  nbgrnself  26470  vtxdginducedm1  26666  isgrpoi  27680  isvciOLD  27762  cnidOLD  27764  isnvi  27795  ipasslem8  28019  hilid  28345  hlimf  28421  shsspwh  28430  pjrni  28888  pjmf1  28902  df0op2  28938  dfiop2  28939  hoaddcomi  28958  hoaddassi  28962  hocadddiri  28965  hocsubdiri  28966  hoaddid1i  28972  ho0coi  28974  hoid1i  28975  hoid1ri  28976  honegsubi  28982  hoddii  29175  lnopunilem2  29197  elunop2  29199  lnophm  29205  imaelshi  29244  cnlnadjlem8  29260  pjnmopi  29334  pjsdii  29341  pjddii  29342  pjtoi  29365  chirred  29581  nnindf  29891  nn0min  29893  esum2d  30479  dmvlsiga  30516  volmeas  30618  ddemeas  30623  sxbrsigalem3  30658  coinfliprv  30868  ballotlem7  30921  signsw0glem  30954  rpsqrtcn  30995  tgoldbachgt  31065  bnj580  31304  bnj1384  31421  bnj1497  31449  kur14lem9  31517  msrf  31760  dfon2lem7  32012  frinsg  32064  bdayfo  32147  nodense  32161  fobigcup  32326  nn0prpwlem  32636  topmeet  32678  onsucsuccmpi  32757  taupilemrplb  33481  relowlssretop  33525  ptrecube  33720  poimirlem27  33747  heicant  33755  mblfinlem1  33757  volsupnfl  33765  dvtan  33770  itg2addnc  33774  indexa  33838  sstotbnd2  33882  heiborlem7  33925  atpsubN  35531  idldil  35892  cdleme50ldil  36326  mzpclall  37789  dgraaf  38215  arearect  38298  areaquad  38299  clsk1indlem2  38837  clsk1indlem4  38839  prmunb2  39007  radcnvrat  39010  unirnmapsn  39890  ssmapsn  39892  upbdrech  39997  supminfxr  40170  supminfxr2  40175  supminfxrrnmpt  40177  fsumiunss  40284  resincncf  40565  dmvolss  40678  volioof  40680  stoweidlem57  40750  wallispilem3  40760  stirlinglem13  40779  dirkertrigeqlem3  40793  fourierdlem62  40861  salexct  41028  salexct3  41036  salgencntex  41037  salgensscntex  41038  gsumge0cl  41064  0ome  41222  icoresmbl  41236  hoidmv1le  41287  smflimlem1  41458  smfpimbor1lem2  41485  smfliminflem  41515  fmtno4prm  42059  31prm  42084  tgoldbach  42277  2zlidl  42499  2zrngagrp  42508  2zrngnmlid  42514  crhmsubc  42643  drhmsubc  42645  drngcat  42646  fldcat  42647  fldhmsubc  42649  crhmsubcALTV  42661  drhmsubcALTV  42663  drngcatALTV  42664  fldcatALTV  42665  fldhmsubcALTV  42667  zlmodzxznm  42851  ldepsnlinc  42862  nn0sumshdiglem2  42981  onsetrec  43019
  Copyright terms: Public domain W3C validator