Theorem rgen 3061

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3059

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

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

This theorem is referenced by:  ralel  3062  rgenw  3063  mprg  3065  mprgbir  3066  nrex  3072  rexlimivOLD  3183  rgen2  3197  r19.21be  3250  rexlimi  3257  rgen2a  3369  sbcth2  3893  r19.2zb  4502  unimax  4949  mpteq1OLD  5242  mpteq2iaOLD  5252  reusv2lem4  5407  wfisgOLD  6377  fnopab  6707  fmpti  7132  sorpssuni  7751  sorpssint  7752  onssmin  7812  tfis  7876  omssnlim  7902  finds  7919  finds2  7921  opabex3  7991  wfr3OLD  8377  seqomlem2  8490  findcard3  9316  findcard3OLD  9317  fifo  9470  fisupcl  9507  dfom3  9685  cantnfvalf  9703  frinsg  9789  rankf  9832  scottex  9923  cplem1  9927  harcard  10016  cardiun  10020  r0weon  10050  acnnum  10090  alephon  10107  alephsmo  10140  alephf1ALT  10141  alephfplem4  10145  dfac5lem4  10164  dfac5lem4OLD  10166  dfacacn  10180  kmlem1  10189  cflem  10283  cflemOLD  10284  cflecard  10291  cfsmolem  10308  fin23lem17  10376  hsmexlem4  10467  omina  10729  0tsk  10793  inar1  10813  wfgru  10854  reclem2pr  11086  nnssre  12268  nnsscn  12269  dfnn2  12277  dfnn3  12278  nnind  12282  nnsub  12308  dfuzi  12707  uzsupss  12980  cnref1o  13025  xrsupsslem  13346  xrinfmsslem  13347  xrsup0  13362  reltre  13379  rpltrp  13380  reltxrnmnf  13381  seqexw  14055  ser0f  14093  bccl  14358  hashkf  14368  hashbc  14489  wrdind  14757  01sqrexlem5  15282  sqrtf  15399  ackbijnn  15861  incexclem  15869  prodf1f  15925  eff2  16132  reeff1  16153  sqrt2irr  16282  prmind2  16719  3prm  16728  phisum  16824  pockthi  16941  infpn2  16947  prminf  16949  prmreclem2  16951  prmrec  16956  1arith  16961  1arith2  16962  vdwlem13  17027  ramz  17059  prmgap  17093  prmgaplcm  17094  prmgapprmo  17096  prmlem1a  17141  xpsff1o  17614  isacs1i  17702  dmaf  18103  cdaf  18104  coapm  18125  lublecllem  18418  smndex1mnd  18936  pwmnd  18963  pmtrdifel  19513  pmtrdifwrdel  19518  odf  19570  efgrelexlemb  19783  dprd2da  20077  rngmgpf  20175  mgpf  20266  prdscrngd  20336  crhmsubc  20699  drhmsubc  20799  drngcat  20800  fldcat  20801  fldhmsubc  20803  cnfld1  21424  cnfld1OLD  21425  cnsubglem  21451  cnmsubglem  21466  nn0srg  21473  rge0srg  21474  pzriprnglem4  21513  pzriprnglem9  21518  pzriprnglem14  21523  pmatcoe1fsupp  22723  isbasis3g  22972  basdif0  22976  distop  23018  mretopd  23116  2ndcsep  23483  refref  23537  kqf  23771  fbssfi  23861  filconn  23907  prdstmdd  24148  ustfilxp  24237  prdsxmslem2  24558  qdensere  24806  recld2  24850  isclmi0  25145  iscvsi  25176  ovolf  25531  dyadmax  25647  dveflem  26032  mdegxrf  26122  fta1  26365  vieta1  26369  aalioulem2  26390  taylfval  26415  pilem2  26511  pilem3  26512  recosf1o  26592  divlogrlim  26692  logcn  26704  ressatans  26992  leibpi  27000  ftalem3  27133  chtub  27271  2sqlem6  27482  2sqlem10  27487  2sqreulem4  27513  chtppilim  27534  pntpbnd1  27645  pntlem3  27668  padicabvf  27690  bdayfo  27737  nodense  27752  oldf  27911  scutfo  27957  addsfo  28031  negsf  28099  negsfo  28100  subsfo  28110  dfn0s2  28351  n0subs  28375  dfnns2  28377  zs12bday  28439  axcontlem2  28995  nbgrnself  29391  vtxdginducedm1  29576  isgrpoi  30527  isvciOLD  30609  cnidOLD  30611  isnvi  30642  ipasslem8  30866  hilid  31190  hlimf  31266  shsspwh  31275  pjrni  31731  pjmf1  31745  df0op2  31781  dfiop2  31782  hoaddcomi  31801  hoaddassi  31805  hocadddiri  31808  hocsubdiri  31809  hoaddridi  31815  ho0coi  31817  hoid1i  31818  hoid1ri  31819  honegsubi  31825  hoddii  32018  lnopunilem2  32040  elunop2  32042  lnophm  32048  imaelshi  32087  cnlnadjlem8  32103  pjnmopi  32177  pjsdii  32184  pjddii  32185  pjtoi  32208  chirred  32424  nnindf  32826  nn0min  32827  wrdt2ind  32923  zringfrac  33562  ccfldsrarelvec  33696  constrconj  33750  2sqr3minply  33753  esum2d  34074  dmvlsiga  34110  volmeas  34212  ddemeas  34217  sxbrsigalem3  34254  coinfliprv  34464  ballotlem7  34517  signsw0glem  34547  rpsqrtcn  34587  tgoldbachgt  34657  bnj580  34906  bnj1384  35025  bnj1497  35053  kur14lem9  35199  sat1el2xp  35364  msrf  35527  dfon2lem7  35771  fobigcup  35882  nn0prpwlem  36305  topmeet  36347  onsucsuccmpi  36426  taupilemrplb  37303  relowlssretop  37346  ptrecube  37607  poimirlem27  37634  heicant  37642  mblfinlem1  37644  volsupnfl  37652  dvtan  37657  itg2addnc  37661  indexa  37720  sstotbnd2  37761  heiborlem7  37804  atpsubN  39736  idldil  40097  cdleme50ldil  40531  mzpclall  42715  dgraaf  43136  arearect  43204  areaquad  43205  onintunirab  43216  onsupuni  43218  infordmin  43522  omiscard  43533  clsk1indlem2  44032  clsk1indlem4  44034  mnuunid  44273  mnurndlem1  44277  prmunb2  44307  radcnvrat  44310  trwf  44937  unirnmapsn  45157  ssmapsn  45159  upbdrech  45256  supminfxr  45414  supminfxr2  45419  supminfxrrnmpt  45421  rexanuz2nf  45443  fsumiunss  45531  resincncf  45831  dmvolss  45941  volioof  45943  stoweidlem57  46013  wallispilem3  46023  stirlinglem13  46042  dirkertrigeqlem3  46056  fourierdlem62  46124  salexct  46290  salexct3  46298  salgencntex  46299  salgensscntex  46300  gsumge0cl  46327  0ome  46485  icoresmbl  46499  hoidmv1le  46550  smflimlem1  46727  smfpimbor1lem2  46755  smfliminflem  46786  natlocalincr  46830  ralndv1  47055  fmtno4prm  47500  31prm  47522  tgoldbach  47742  gpg5grlic  47975  nn0mnd  48023  2zlidl  48084  2zrngagrp  48093  2zrngnmlid  48099  crhmsubcALTV  48171  drhmsubcALTV  48173  drngcatALTV  48174  fldcatALTV  48175  fldhmsubcALTV  48177  zlmodzxznm  48343  ldepsnlinc  48354  nn0sumshdiglem2  48472  itcovalpclem1  48520  itcovalt2lem1  48525  rrx2xpref1o  48568  setc2othin  48857  onsetrec  48939