Theorem rgen 3046

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 3045	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		rgen.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	mpgbir 1799	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  ralel  3047  rgenw  3048  mprg  3050  mprgbir  3051  nrex  3057  rgen2  3169  r19.21be  3222  rexlimi  3229  rgen2a  3336  sbcth2  3838  r19.2zb  4449  unimax  4897  reusv2lem4  5343  fnopab  6624  fmpti  7050  sorpssuni  7672  sorpssint  7673  onssmin  7732  tfis  7795  omssnlim  7821  finds  7836  finds2  7838  opabex3  7909  seqomlem2  8380  findcard3  9187  findcard3OLD  9188  fifo  9341  fisupcl  9379  dfom3  9562  cantnfvalf  9580  frinsg  9666  rankf  9709  scottex  9800  cplem1  9804  harcard  9893  cardiun  9897  r0weon  9925  acnnum  9965  alephon  9982  alephsmo  10015  alephf1ALT  10016  alephfplem4  10020  dfac5lem4  10039  dfac5lem4OLD  10041  dfacacn  10055  kmlem1  10064  cflem  10158  cflemOLD  10159  cflecard  10166  cfsmolem  10183  fin23lem17  10251  hsmexlem4  10342  omina  10604  0tsk  10668  inar1  10688  wfgru  10729  reclem2pr  10961  nnssre  12150  nnsscn  12151  dfnn2  12159  dfnn3  12160  nnind  12164  nnsub  12190  dfuzi  12585  uzsupss  12859  cnref1o  12904  xrsupsslem  13227  xrinfmsslem  13228  xrsup0  13243  reltre  13261  rpltrp  13262  reltxrnmnf  13263  seqexw  13942  ser0f  13980  bccl  14247  hashkf  14257  hashbc  14378  wrdind  14646  01sqrexlem5  15171  sqrtf  15289  ackbijnn  15753  incexclem  15761  prodf1f  15817  eff2  16026  reeff1  16047  sqrt2irr  16176  prmind2  16614  3prm  16623  phisum  16720  pockthi  16837  infpn2  16843  prminf  16845  prmreclem2  16847  prmrec  16852  1arith  16857  1arith2  16858  vdwlem13  16923  ramz  16955  prmgap  16989  prmgaplcm  16990  prmgapprmo  16992  prmlem1a  17036  xpsff1o  17489  isacs1i  17581  dmaf  17974  cdaf  17975  coapm  17996  lublecllem  18282  smndex1mnd  18802  pwmnd  18829  pmtrdifel  19377  pmtrdifwrdel  19382  odf  19434  efgrelexlemb  19647  dprd2da  19941  rngmgpf  20060  mgpf  20151  prdscrngd  20225  crhmsubc  20585  drhmsubc  20684  drngcat  20685  fldcat  20686  fldhmsubc  20688  cnfld1  21318  cnfld1OLD  21319  cnsubglem  21340  cnmsubglem  21355  nn0srg  21362  rge0srg  21363  pzriprnglem4  21409  pzriprnglem9  21414  pzriprnglem14  21419  pmatcoe1fsupp  22604  isbasis3g  22852  basdif0  22856  distop  22898  mretopd  22995  2ndcsep  23362  refref  23416  kqf  23650  fbssfi  23740  filconn  23786  prdstmdd  24027  ustfilxp  24116  prdsxmslem2  24433  qdensere  24673  recld2  24719  isclmi0  25014  iscvsi  25045  ovolf  25399  dyadmax  25515  dveflem  25899  mdegxrf  25989  fta1  26232  vieta1  26236  aalioulem2  26257  taylfval  26282  pilem2  26378  pilem3  26379  recosf1o  26460  divlogrlim  26560  logcn  26572  ressatans  26860  leibpi  26868  ftalem3  27001  chtub  27139  2sqlem6  27350  2sqlem10  27355  2sqreulem4  27381  chtppilim  27402  pntpbnd1  27513  pntlem3  27536  padicabvf  27558  bdayfo  27605  nodense  27620  oldf  27785  scutfo  27837  addsfo  27913  negsf  27981  negsfo  27982  subsfo  27992  onsiso  28192  dfn0s2  28247  n0subs  28276  bdayn0sf1o  28282  dfnns2  28284  zsoring  28319  zs12zodd  28377  zs12bday  28379  axcontlem2  28928  nbgrnself  29322  vtxdginducedm1  29507  isgrpoi  30460  isvciOLD  30542  cnidOLD  30544  isnvi  30575  ipasslem8  30799  hilid  31123  hlimf  31199  shsspwh  31208  pjrni  31664  pjmf1  31678  df0op2  31714  dfiop2  31715  hoaddcomi  31734  hoaddassi  31738  hocadddiri  31741  hocsubdiri  31742  hoaddridi  31748  ho0coi  31750  hoid1i  31751  hoid1ri  31752  honegsubi  31758  hoddii  31951  lnopunilem2  31973  elunop2  31975  lnophm  31981  imaelshi  32020  cnlnadjlem8  32036  pjnmopi  32110  pjsdii  32117  pjddii  32118  pjtoi  32141  chirred  32357  nnindf  32777  nn0min  32778  wrdt2ind  32908  zringfrac  33504  ccfldsrarelvec  33645  constrconj  33714  2sqr3minply  33749  cos9thpiminply  33757  esum2d  34062  dmvlsiga  34098  volmeas  34200  ddemeas  34205  sxbrsigalem3  34242  coinfliprv  34453  ballotlem7  34506  signsw0glem  34523  rpsqrtcn  34563  tgoldbachgt  34633  bnj580  34882  bnj1384  35001  bnj1497  35029  onvf1odlem1  35078  kur14lem9  35189  sat1el2xp  35354  msrf  35517  dfon2lem7  35765  fobigcup  35876  nn0prpwlem  36298  topmeet  36340  onsucsuccmpi  36419  taupilemrplb  37296  relowlssretop  37339  ptrecube  37602  poimirlem27  37629  heicant  37637  mblfinlem1  37639  volsupnfl  37647  dvtan  37652  itg2addnc  37656  indexa  37715  sstotbnd2  37756  heiborlem7  37799  atpsubN  39735  idldil  40096  cdleme50ldil  40530  mzpclall  42703  dgraaf  43123  arearect  43191  areaquad  43192  onintunirab  43203  onsupuni  43205  infordmin  43508  omiscard  43519  clsk1indlem2  44018  clsk1indlem4  44020  mnuunid  44253  mnurndlem1  44257  prmunb2  44287  radcnvrat  44290  trwf  44936  rankrelp  44937  wfac8prim  44979  unirnmapsn  45195  ssmapsn  45197  upbdrech  45290  supminfxr  45447  supminfxr2  45452  supminfxrrnmpt  45454  rexanuz2nf  45475  fsumiunss  45560  resincncf  45860  dmvolss  45970  volioof  45972  stoweidlem57  46042  wallispilem3  46052  stirlinglem13  46071  dirkertrigeqlem3  46085  fourierdlem62  46153  salexct  46319  salexct3  46327  salgencntex  46328  salgensscntex  46329  gsumge0cl  46356  0ome  46514  icoresmbl  46528  hoidmv1le  46579  smflimlem1  46756  smfpimbor1lem2  46784  smfliminflem  46815  natlocalincr  46861  sinnpoly  46879  ralndv1  47093  fmtno4prm  47563  31prm  47585  tgoldbach  47805  gpg5grlim  48081  gpg5grlic  48082  nn0mnd  48167  2zlidl  48228  2zrngagrp  48237  2zrngnmlid  48243  crhmsubcALTV  48315  drhmsubcALTV  48317  drngcatALTV  48318  fldcatALTV  48319  fldhmsubcALTV  48321  zlmodzxznm  48486  ldepsnlinc  48497  nn0sumshdiglem2  48611  itcovalpclem1  48659  itcovalt2lem1  48664  rrx2xpref1o  48707  slotresfo  48887  basresposfo  48966  oppff1  49137  setc2othin  49455  setcsnterm  49479  onsetrec  49697