Theorem rgen 3064

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  ralel  3065  rgenw  3066  mprg  3068  mprgbir  3069  nrex  3075  rexlimivOLD  3185  rgen2  3198  r19.21be  3250  rexlimi  3257  rgen2a  3368  sbcth2  3877  r19.2zb  4494  ral0OLD  4515  unimax  4947  mpteq1OLD  5241  mpteq2iaOLD  5251  reusv2lem4  5398  wfisgOLD  6352  fnopab  6685  fmpti  7107  sorpssuni  7717  sorpssint  7718  onssmin  7775  tfis  7839  omssnlim  7865  finds  7884  finds2  7886  opabex3  7949  wfr3OLD  8333  seqomlem2  8446  findcard3  9281  findcard3OLD  9282  fifo  9423  fisupcl  9460  dfom3  9638  cantnfvalf  9656  frinsg  9742  rankf  9785  scottex  9876  cplem1  9880  harcard  9969  cardiun  9973  r0weon  10003  acnnum  10043  alephon  10060  alephsmo  10093  alephf1ALT  10094  alephfplem4  10098  dfac5lem4  10117  dfacacn  10132  kmlem1  10141  cflem  10237  cflecard  10244  cfsmolem  10261  fin23lem17  10329  hsmexlem4  10420  omina  10682  0tsk  10746  inar1  10766  wfgru  10807  reclem2pr  11039  nnssre  12212  nnsscn  12213  dfnn2  12221  dfnn3  12222  nnind  12226  nnsub  12252  dfuzi  12649  uzsupss  12920  cnref1o  12965  xrsupsslem  13282  xrinfmsslem  13283  xrsup0  13298  reltre  13315  rpltrp  13316  reltxrnmnf  13317  seqexw  13978  ser0f  14017  bccl  14278  hashkf  14288  hashbc  14408  wrdind  14668  01sqrexlem5  15189  sqrtf  15306  ackbijnn  15770  incexclem  15778  prodf1f  15834  eff2  16038  reeff1  16059  sqrt2irr  16188  prmind2  16618  3prm  16627  phisum  16719  pockthi  16836  infpn2  16842  prminf  16844  prmreclem2  16846  prmrec  16851  1arith  16856  1arith2  16857  vdwlem13  16922  ramz  16954  prmgap  16988  prmgaplcm  16989  prmgapprmo  16991  prmlem1a  17036  xpsff1o  17509  isacs1i  17597  dmaf  17995  cdaf  17996  coapm  18017  lublecllem  18309  smndex1mnd  18787  pwmnd  18814  pmtrdifel  19341  pmtrdifwrdel  19346  odf  19398  efgrelexlemb  19611  dprd2da  19904  mgpf  20062  prdscrngd  20125  cnfld1  20955  cnsubglem  20979  cnmsubglem  20993  nn0srg  21000  rge0srg  21001  pmatcoe1fsupp  22185  isbasis3g  22434  basdif0  22438  distop  22480  mretopd  22578  2ndcsep  22945  refref  22999  kqf  23233  fbssfi  23323  filconn  23369  prdstmdd  23610  ustfilxp  23699  prdsxmslem2  24020  qdensere  24268  recld2  24312  isclmi0  24596  iscvsi  24627  ovolf  24981  dyadmax  25097  dveflem  25478  mdegxrf  25568  fta1  25803  vieta1  25807  aalioulem2  25828  taylfval  25853  pilem2  25946  pilem3  25947  recosf1o  26026  divlogrlim  26125  logcn  26137  ressatans  26419  leibpi  26427  ftalem3  26559  chtub  26695  2sqlem6  26906  2sqlem10  26911  2sqreulem4  26937  chtppilim  26958  pntpbnd1  27069  pntlem3  27092  padicabvf  27114  bdayfo  27160  nodense  27175  oldf  27332  scutfo  27378  addsfo  27447  negsf  27506  negsfo  27507  axcontlem2  28203  nbgrnself  28596  vtxdginducedm1  28780  isgrpoi  29729  isvciOLD  29811  cnidOLD  29813  isnvi  29844  ipasslem8  30068  hilid  30392  hlimf  30468  shsspwh  30477  pjrni  30933  pjmf1  30947  df0op2  30983  dfiop2  30984  hoaddcomi  31003  hoaddassi  31007  hocadddiri  31010  hocsubdiri  31011  hoaddridi  31017  ho0coi  31019  hoid1i  31020  hoid1ri  31021  honegsubi  31027  hoddii  31220  lnopunilem2  31242  elunop2  31244  lnophm  31250  imaelshi  31289  cnlnadjlem8  31305  pjnmopi  31379  pjsdii  31386  pjddii  31387  pjtoi  31410  chirred  31626  nnindf  32003  nn0min  32004  wrdt2ind  32095  ccfldsrarelvec  32690  esum2d  33029  dmvlsiga  33065  volmeas  33167  ddemeas  33172  sxbrsigalem3  33209  coinfliprv  33419  ballotlem7  33472  signsw0glem  33502  rpsqrtcn  33543  tgoldbachgt  33613  bnj580  33862  bnj1384  33981  bnj1497  34009  kur14lem9  34143  sat1el2xp  34308  msrf  34471  dfon2lem7  34699  fobigcup  34810  nn0prpwlem  35145  topmeet  35187  onsucsuccmpi  35266  taupilemrplb  36139  relowlssretop  36182  ptrecube  36426  poimirlem27  36453  heicant  36461  mblfinlem1  36463  volsupnfl  36471  dvtan  36476  itg2addnc  36480  indexa  36539  sstotbnd2  36580  heiborlem7  36623  atpsubN  38562  idldil  38923  cdleme50ldil  39357  mzpclall  41398  dgraaf  41822  arearect  41897  areaquad  41898  onintunirab  41909  onsupuni  41911  infordmin  42216  omiscard  42227  clsk1indlem2  42726  clsk1indlem4  42728  mnuunid  42969  mnurndlem1  42973  prmunb2  43003  radcnvrat  43006  unirnmapsn  43846  ssmapsn  43848  upbdrech  43950  supminfxr  44109  supminfxr2  44114  supminfxrrnmpt  44116  rexanuz2nf  44138  fsumiunss  44226  resincncf  44526  dmvolss  44636  volioof  44638  stoweidlem57  44708  wallispilem3  44718  stirlinglem13  44737  dirkertrigeqlem3  44751  fourierdlem62  44819  salexct  44985  salexct3  44993  salgencntex  44994  salgensscntex  44995  gsumge0cl  45022  0ome  45180  icoresmbl  45194  hoidmv1le  45245  smflimlem1  45422  smfpimbor1lem2  45450  smfliminflem  45481  natlocalincr  45525  ralndv1  45748  fmtno4prm  46178  31prm  46200  tgoldbach  46420  nn0mnd  46524  rngmgpf  46588  2zlidl  46734  2zrngagrp  46743  2zrngnmlid  46749  crhmsubc  46878  drhmsubc  46880  drngcat  46881  fldcat  46882  fldhmsubc  46884  crhmsubcALTV  46896  drhmsubcALTV  46898  drngcatALTV  46899  fldcatALTV  46900  fldhmsubcALTV  46902  zlmodzxznm  47080  ldepsnlinc  47091  nn0sumshdiglem2  47210  itcovalpclem1  47258  itcovalt2lem1  47263  rrx2xpref1o  47306  setc2othin  47578  onsetrec  47655