Theorem rgen 3053

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3051

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

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

This theorem is referenced by:  ralel  3054  rgenw  3055  mprg  3057  mprgbir  3058  nrex  3065  rgen2  3177  r19.21be  3230  rexlimi  3237  rgen2a  3333  sbcth2  3822  unimax  4887  reusv2lem4  5343  fnopab  6636  fmpti  7064  sorpssuni  7686  sorpssint  7687  onssmin  7746  tfis  7806  omssnlim  7832  finds  7847  finds2  7849  opabex3  7920  seqomlem2  8390  findcard3  9193  fifo  9345  fisupcl  9383  dfom3  9568  cantnfvalf  9586  frinsg  9675  rankf  9718  scottex  9809  cplem1  9813  harcard  9902  cardiun  9906  r0weon  9934  acnnum  9974  alephon  9991  alephsmo  10024  alephf1ALT  10025  alephfplem4  10029  dfac5lem4  10048  dfac5lem4OLD  10050  dfacacn  10064  kmlem1  10073  cflem  10167  cflemOLD  10168  cflecard  10175  cfsmolem  10192  fin23lem17  10260  hsmexlem4  10351  omina  10614  0tsk  10678  inar1  10698  wfgru  10739  reclem2pr  10971  nnssre  12178  nnsscn  12179  dfnn2  12187  dfnn3  12188  nnind  12192  nnsub  12221  dfuzi  12620  uzsupss  12890  cnref1o  12935  xrsupsslem  13259  xrinfmsslem  13260  xrsup0  13275  reltre  13293  rpltrp  13294  reltxrnmnf  13295  seqexw  13979  ser0f  14017  bccl  14284  hashkf  14294  hashbc  14415  wrdind  14684  01sqrexlem5  15208  sqrtf  15326  ackbijnn  15793  incexclem  15801  prodf1f  15857  eff2  16066  reeff1  16087  sqrt2irr  16216  prmind2  16654  3prm  16663  phisum  16761  pockthi  16878  infpn2  16884  prminf  16886  prmreclem2  16888  prmrec  16893  1arith  16898  1arith2  16899  vdwlem13  16964  ramz  16996  prmgap  17030  prmgaplcm  17031  prmgapprmo  17033  prmlem1a  17077  xpsff1o  17531  isacs1i  17623  dmaf  18016  cdaf  18017  coapm  18038  lublecllem  18324  chninf  18601  ex-chn1  18603  ex-chn2  18604  smndex1mnd  18881  pwmnd  18908  pmtrdifel  19455  pmtrdifwrdel  19460  odf  19512  efgrelexlemb  19725  dprd2da  20019  rngmgpf  20138  mgpf  20229  prdscrngd  20301  crhmsubc  20659  drhmsubc  20758  drngcat  20759  fldcat  20760  fldhmsubc  20762  cnfld1  21377  cnsubglem  21396  cnmsubglem  21410  nn0srg  21417  rge0srg  21418  pzriprnglem4  21464  pzriprnglem9  21469  pzriprnglem14  21474  pmatcoe1fsupp  22666  isbasis3g  22914  basdif0  22918  distop  22960  mretopd  23057  2ndcsep  23424  refref  23478  kqf  23712  fbssfi  23802  filconn  23848  prdstmdd  24089  ustfilxp  24178  prdsxmslem2  24494  qdensere  24734  recld2  24780  isclmi0  25065  iscvsi  25096  ovolf  25449  dyadmax  25565  dveflem  25946  mdegxrf  26033  fta1  26274  vieta1  26278  aalioulem2  26299  taylfval  26324  pilem2  26417  pilem3  26418  recosf1o  26499  divlogrlim  26599  logcn  26611  ressatans  26898  leibpi  26906  ftalem3  27038  chtub  27175  2sqlem6  27386  2sqlem10  27391  2sqreulem4  27417  chtppilim  27438  pntpbnd1  27549  pntlem3  27572  padicabvf  27594  bdayfo  27641  nodense  27656  oldf  27829  cutsfo  27897  addsfo  27975  negsf  28044  negsfo  28045  subsfo  28057  oniso  28263  dfn0s2  28324  n0subs  28355  bdayn0sf1o  28362  dfnns2  28364  zsoring  28401  bdaypw2n0bndlem  28455  bdayfinbndlem2  28460  z12zsodd  28474  axcontlem2  29034  nbgrnself  29428  vtxdginducedm1  29612  isgrpoi  30569  isvciOLD  30651  cnidOLD  30653  isnvi  30684  ipasslem8  30908  hilid  31232  hlimf  31308  shsspwh  31317  pjrni  31773  pjmf1  31787  df0op2  31823  dfiop2  31824  hoaddcomi  31843  hoaddassi  31847  hocadddiri  31850  hocsubdiri  31851  hoaddridi  31857  ho0coi  31859  hoid1i  31860  hoid1ri  31861  honegsubi  31867  hoddii  32060  lnopunilem2  32082  elunop2  32084  lnophm  32090  imaelshi  32129  cnlnadjlem8  32145  pjnmopi  32219  pjsdii  32226  pjddii  32227  pjtoi  32250  chirred  32466  nnindf  32893  nn0min  32894  wrdt2ind  33013  zringfrac  33614  ccfldsrarelvec  33815  constrconj  33889  2sqr3minply  33924  cos9thpiminply  33932  esum2d  34237  dmvlsiga  34273  volmeas  34375  ddemeas  34380  sxbrsigalem3  34416  coinfliprv  34627  ballotlem7  34680  signsw0glem  34697  rpsqrtcn  34737  tgoldbachgt  34807  bnj580  35055  bnj1384  35174  bnj1497  35202  fineqvnttrclse  35268  onvf1odlem1  35285  kur14lem9  35396  sat1el2xp  35561  msrf  35724  dfon2lem7  35969  fobigcup  36080  nn0prpwlem  36504  topmeet  36546  onsucsuccmpi  36625  dfttc4lem2  36711  taupilemrplb  37634  relowlssretop  37679  ptrecube  37941  poimirlem27  37968  heicant  37976  mblfinlem1  37978  volsupnfl  37986  dvtan  37991  itg2addnc  37995  indexa  38054  sstotbnd2  38095  heiborlem7  38138  disjimeceqim  39125  atpsubN  40199  idldil  40560  cdleme50ldil  40994  mzpclall  43159  dgraaf  43575  arearect  43643  areaquad  43644  onintunirab  43655  onsupuni  43657  infordmin  43959  omiscard  43970  clsk1indlem2  44469  clsk1indlem4  44471  mnuunid  44704  mnurndlem1  44708  prmunb2  44738  radcnvrat  44741  trwf  45386  rankrelp  45387  wfac8prim  45429  unirnmapsn  45643  ssmapsn  45645  upbdrech  45738  supminfxr  45892  supminfxr2  45897  supminfxrrnmpt  45899  rexanuz2nf  45920  fsumiunss  46005  resincncf  46303  dmvolss  46413  volioof  46415  stoweidlem57  46485  wallispilem3  46495  stirlinglem13  46514  dirkertrigeqlem3  46528  fourierdlem62  46596  salexct  46762  salexct3  46770  salgencntex  46771  salgensscntex  46772  gsumge0cl  46799  0ome  46957  icoresmbl  46971  hoidmv1le  47022  smflimlem1  47199  smfpimbor1lem2  47227  smfliminflem  47258  natlocalincr  47306  sinnpoly  47339  ralndv1  47553  fmtno4prm  48038  31prm  48060  tgoldbach  48293  gpg5grlim  48569  gpg5grlic  48570  nn0mnd  48655  2zlidl  48716  2zrngagrp  48725  2zrngnmlid  48731  crhmsubcALTV  48803  drhmsubcALTV  48805  drngcatALTV  48806  fldcatALTV  48807  fldhmsubcALTV  48809  zlmodzxznm  48973  ldepsnlinc  48984  nn0sumshdiglem2  49098  itcovalpclem1  49146  itcovalt2lem1  49151  rrx2xpref1o  49194  slotresfo  49374  basresposfo  49453  oppff1  49623  setc2othin  49941  setcsnterm  49965  onsetrec  50183