Theorem rgen 3080

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

Step	Hyp	Ref	Expression
1		df-ral 3079	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		rgen.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	mpgbir 1832	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  ralel  3081  rgenw  3082  mprg  3084  mprgbir  3085  nrex  3092  rgen2  3204  r19.21be  3257  rexlimi  3264  rgen2a  3358  sbcth2  3834  unimax  4908  reusv2lem4  5370  fnopab  6674  fmpti  7109  sorpssuni  7737  sorpssint  7738  onssmin  7795  tfis  7855  omssnlim  7881  finds  7897  finds2  7899  opabex3  7968  seqomlem2  8444  findcard3  9257  fifo  9406  fisupcl  9444  dfom3  9630  cantnfvalf  9648  frinsg  9737  rankf  9780  scottex  9876  scottexOLD  9877  cplem1  9893  cplem1OLD  9894  harcard  9987  cardiun  9991  r0weon  10019  acnnum  10059  alephon  10076  alephsmo  10109  alephf1ALT  10110  alephfplem4  10114  dfac5lem4  10133  dfacacn  10148  kmlem1  10157  cflem  10251  cflecard  10258  cfsmolem  10276  fin23lem17  10344  hsmexlem4  10435  omina  10704  0tsk  10768  inar1  10788  wfgru  10829  reclem2pr  11061  nnssre  12265  nnsscn  12266  dfnn2  12274  dfnn3  12275  nnind  12279  nnsub  12308  dfuzi  12716  uzsupss  12993  cnref1o  13039  xrsupsslem  13363  xrinfmsslem  13364  xrsup0  13379  reltre  13397  rpltrp  13398  reltxrnmnf  13399  seqexw  14085  ser0f  14123  bccl  14390  hashkf  14400  hashbc  14522  wrdind  14795  sgnrn  15175  01sqrexlem5  15337  sqrtf  15455  ackbijnn  15921  incexclem  15929  prodf1f  15985  eff2  16193  reeff1  16214  sqrt2irr  16343  prmind2  16781  3prm  16790  phisum  16888  pockthi  17005  infpn2  17011  prminf  17013  prmreclem2  17015  prmrec  17020  1arith  17025  1arith2  17026  vdwlem13  17091  ramz  17123  prmgap  17157  prmgaplcm  17158  prmgapprmo  17160  prmlem1a  17204  xpsff1o  17659  isacs1i  17751  dmaf  18144  cdaf  18145  coapm  18166  lublecllem  18452  chninf  18729  ex-chn1  18731  ex-chn2  18732  smndex1mnd  19028  pwmnd  19062  pmtrdifel  19613  pmtrdifwrdel  19618  odf  19670  efgrelexlemb  19883  dprd2da  20177  rngmgpf  20298  mgpf  20393  prdscrngd  20468  crhmsubc  20850  drhmsubc  20953  drngcat  20954  fldcat  20955  fldhmsubc  20957  cnfld1  21616  cnsubglem  21635  cnmsubglem  21649  nn0srg  21656  rge0srg  21657  pzriprnglem4  21703  pzriprnglem9  21708  pzriprnglem14  21713  pmatcoe1fsupp  22932  isbasis3g  23180  basdif0  23184  distop  23226  mretopd  23323  2ndcsep  23691  refref  23745  kqf  23979  fbssfi  24069  filconn  24115  prdstmdd  24356  ustfilxp  24445  prdsxmslem2  24761  qdensere  25001  recld2  25047  isclmi0  25332  iscvsi  25363  ovolf  25716  dyadmax  25832  dveflem  26213  mdegxrf  26300  fta1  26545  vieta1  26551  aalioulem2  26576  taylfval  26602  pilem2  26695  pilem3  26696  recosf1o  26780  divlogrlim  26880  logcn  26892  ressatans  27179  leibpi  27187  ftalem3  27319  chtub  27456  2sqlem6  27667  2sqlem10  27672  2sqreulem4  27698  chtppilim  27719  pntpbnd1  27830  pntlem3  27853  padicabvf  27875  bdayfo  27921  nodense  27936  oldf  28110  cutsfo  28178  addsfo  28256  negsf  28325  negsfo  28326  subsfo  28338  oniso  28544  dfn0s2  28605  n0subs  28636  bdayn0sf1o  28643  dfnns2  28645  zsoring  28682  bdaypw2n0bndlem  28736  bdayfinbndlem2  28741  z12zsodd  28755  axcontlem2  29430  nbgrnself  29827  vtxdginducedm1  30011  isgrpoi  30987  isvciOLD  31069  cnidOLD  31071  isnvi  31102  ipasslem8  31326  hilid  31650  hlimf  31726  shsspwh  31735  pjrni  32191  pjmf1  32205  df0op2  32241  dfiop2  32242  hoaddcomi  32261  hoaddassi  32265  hocadddiri  32268  hocsubdiri  32269  hoaddridi  32275  ho0coi  32277  hoid1i  32278  hoid1ri  32279  honegsubi  32285  hoddii  32478  lnopunilem2  32500  elunop2  32502  lnophm  32508  imaelshi  32547  cnlnadjlem8  32563  pjnmopi  32637  pjsdii  32644  pjddii  32645  pjtoi  32668  chirred  32884  nnindf  33298  nn0min  33299  wrdt2ind  33403  zringfrac  33972  ccfldsrarelvec  34189  constrconj  34263  2sqr3minply  34298  cos9thpiminply  34306  esum2d  34611  dmvlsiga  34647  volmeas  34750  ddemeas  34755  sxbrsigalem3  34791  coinfliprv  35002  ballotlem7  35055  signsw0glem  35069  rpsqrtcn  35109  tgoldbachgt  35179  bnj580  35430  bnj1384  35549  bnj1497  35577  rankfo  35627  fineqvnttrclse  35658  onvf1odlem1  35708  kur14lem9  35801  sat1el2xp  35966  msrf  36129  dfon2lem7  36374  fobigcup  36485  nn0prpwlem  36949  topmeet  36991  onsucsuccmpi  37070  dfttc4lem2  37156  taupilemrplb  38080  relowlssretop  38125  ptrecube  38377  poimirlem27  38404  heicant  38412  mblfinlem1  38414  volsupnfl  38422  dvtan  38427  itg2addnc  38431  indexa  38491  sstotbnd2  38532  heiborlem7  38575  disjimeceqim  39560  atpsubN  40634  idldil  40995  cdleme50ldil  41429  mzpclall  43580  dgraaf  43996  arearect  44064  areaquad  44065  onintunirab  44076  onsupuni  44078  infordmin  44380  omiscard  44391  clsk1indlem2  44890  clsk1indlem4  44892  mnuunid  45109  mnurndlem1  45113  prmunb2  45143  radcnvrat  45146  trwf  45790  rankrelp  45791  wfac8prim  45833  unirnmapsn  46052  ssmapsn  46054  upbdrech  46146  supminfxr  46300  supminfxr2  46305  supminfxrrnmpt  46307  rexanuz2nf  46328  fsumiunss  46413  resincncf  46711  dmvolss  46821  volioof  46823  stoweidlem57  46893  wallispilem3  46903  stirlinglem13  46922  dirkertrigeqlem3  46936  fourierdlem62  47004  salexct  47170  salexct3  47178  salgencntex  47179  salgensscntex  47180  gsumge0cl  47207  0ome  47365  icoresmbl  47379  hoidmv1le  47430  smflimlem1  47607  smfpimbor1lem2  47635  smfliminflem  47666  ralndv1  48001  fmtno4prm  48486  31prm  48508  tgoldbach  48741  gpg5grlim  49017  gpg5grlic  49018  nn0mnd  49102  2zlidl  49163  2zrngagrp  49172  2zrngnmlid  49178  crhmsubcALTV  49250  drhmsubcALTV  49252  drngcatALTV  49253  fldcatALTV  49254  fldhmsubcALTV  49256  zlmodzxznm  49435  ldepsnlinc  49446  nn0sumshdiglem2  49560  itcovalpclem1  49608  itcovalt2lem1  49613  rrx2xpref1o  49656  slotresfo  49833  basresposfo  49912  oppff1  50082  setc2othin  50400  setcsnterm  50424  onsetrec  50642