Theorem rgen 3116

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106

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 210  df-ral 3111

This theorem is referenced by:  ralel  3117  rgenw  3118  mprg  3120  mprgbir  3121  rgen2  3168  r19.21be  3174  rgen2a  3193  nrex  3228  rexlimiv  3239  rexlimi  3274  sbcth2  3813  r19.2zb  4399  ral0  4414  unimax  4836  mpteq1  5118  mpteq2ia  5121  reusv2lem4  5267  wfisg  6151  fnopab  6458  fmpti  6853  sorpssuni  7438  sorpssint  7439  onssmin  7492  tfis  7549  omssnlim  7574  finds  7589  finds2  7591  opabex3  7650  wfr3  7958  seqomlem2  8070  findcard3  8745  fifo  8880  fisupcl  8917  dfom3  9094  cantnfvalf  9112  rankf  9207  scottex  9298  cplem1  9302  harcard  9391  cardiun  9395  r0weon  9423  acnnum  9463  alephon  9480  alephsmo  9513  alephf1ALT  9514  alephfplem4  9518  dfac5lem4  9537  dfacacn  9552  kmlem1  9561  cflem  9657  cflecard  9664  cfsmolem  9681  fin23lem17  9749  hsmexlem4  9840  omina  10102  0tsk  10166  inar1  10186  wfgru  10227  reclem2pr  10459  nnssre  11629  nnsscn  11630  dfnn2  11638  dfnn3  11639  nnind  11643  nnsub  11669  dfuzi  12061  uzsupss  12328  cnref1o  12372  xrsupsslem  12688  xrinfmsslem  12689  xrsup0  12704  reltre  12721  rpltrp  12722  reltxrnmnf  12723  seqexw  13380  ser0f  13419  bccl  13678  hashkf  13688  hashbc  13807  wrdind  14075  sqrlem5  14598  sqrtf  14715  ackbijnn  15175  incexclem  15183  prodf1f  15240  eff2  15444  reeff1  15465  sqrt2irr  15594  prmind2  16019  3prm  16028  phisum  16117  pockthi  16233  infpn2  16239  prminf  16241  prmreclem2  16243  prmrec  16248  1arith  16253  1arith2  16254  vdwlem13  16319  ramz  16351  prmgap  16385  prmgaplcm  16386  prmgapprmo  16388  prmlem1a  16432  xpsff1o  16832  isacs1i  16920  dmaf  17301  cdaf  17302  coapm  17323  lublecllem  17590  smndex1mnd  18067  pwmnd  18094  pmtrdifel  18600  pmtrdifwrdel  18605  odf  18657  efgrelexlemb  18868  dprd2da  19157  mgpf  19305  prdscrngd  19359  cnfld1  20116  cnsubglem  20140  cnmsubglem  20154  nn0srg  20161  rge0srg  20162  pmatcoe1fsupp  21306  isbasis3g  21554  basdif0  21558  distop  21600  mretopd  21697  2ndcsep  22064  refref  22118  kqf  22352  fbssfi  22442  filconn  22488  prdstmdd  22729  ustfilxp  22818  prdsxmslem2  23136  qdensere  23375  recld2  23419  isclmi0  23703  iscvsi  23734  ovolf  24086  dyadmax  24202  dveflem  24582  mdegxrf  24669  fta1  24904  vieta1  24908  aalioulem2  24929  taylfval  24954  pilem2  25047  pilem3  25048  recosf1o  25127  divlogrlim  25226  logcn  25238  ressatans  25520  leibpi  25528  ftalem3  25660  chtub  25796  2sqlem6  26007  2sqlem10  26012  2sqreulem4  26038  chtppilim  26059  pntpbnd1  26170  pntlem3  26193  padicabvf  26215  axcontlem2  26759  nbgrnself  27149  vtxdginducedm1  27333  isgrpoi  28281  isvciOLD  28363  cnidOLD  28365  isnvi  28396  ipasslem8  28620  hilid  28944  hlimf  29020  shsspwh  29029  pjrni  29485  pjmf1  29499  df0op2  29535  dfiop2  29536  hoaddcomi  29555  hoaddassi  29559  hocadddiri  29562  hocsubdiri  29563  hoaddid1i  29569  ho0coi  29571  hoid1i  29572  hoid1ri  29573  honegsubi  29579  hoddii  29772  lnopunilem2  29794  elunop2  29796  lnophm  29802  imaelshi  29841  cnlnadjlem8  29857  pjnmopi  29931  pjsdii  29938  pjddii  29939  pjtoi  29962  chirred  30178  nnindf  30561  nn0min  30562  wrdt2ind  30653  ccfldsrarelvec  31144  esum2d  31462  dmvlsiga  31498  volmeas  31600  ddemeas  31605  sxbrsigalem3  31640  coinfliprv  31850  ballotlem7  31903  signsw0glem  31933  rpsqrtcn  31974  tgoldbachgt  32044  bnj580  32295  bnj1384  32414  bnj1497  32442  kur14lem9  32574  sat1el2xp  32739  msrf  32902  dfon2lem7  33147  frinsg  33200  bdayfo  33295  nodense  33309  fobigcup  33474  nn0prpwlem  33783  topmeet  33825  onsucsuccmpi  33904  taupilemrplb  34734  relowlssretop  34780  ptrecube  35057  poimirlem27  35084  heicant  35092  mblfinlem1  35094  volsupnfl  35102  dvtan  35107  itg2addnc  35111  indexa  35171  sstotbnd2  35212  heiborlem7  35255  atpsubN  37049  idldil  37410  cdleme50ldil  37844  mzpclall  39668  dgraaf  40091  arearect  40165  areaquad  40166  infordmin  40240  clsk1indlem2  40745  clsk1indlem4  40747  mnuunid  40985  mnurndlem1  40989  prmunb2  41015  radcnvrat  41018  unirnmapsn  41843  ssmapsn  41845  upbdrech  41937  supminfxr  42103  supminfxr2  42108  supminfxrrnmpt  42110  fsumiunss  42217  resincncf  42517  dmvolss  42627  volioof  42629  stoweidlem57  42699  wallispilem3  42709  stirlinglem13  42728  dirkertrigeqlem3  42742  fourierdlem62  42810  salexct  42974  salexct3  42982  salgencntex  42983  salgensscntex  42984  gsumge0cl  43010  0ome  43168  icoresmbl  43182  hoidmv1le  43233  smflimlem1  43404  smfpimbor1lem2  43431  smfliminflem  43461  ralndv1  43661  fmtno4prm  44092  31prm  44114  tgoldbach  44335  nn0mnd  44439  2zlidl  44558  2zrngagrp  44567  2zrngnmlid  44573  crhmsubc  44702  drhmsubc  44704  drngcat  44705  fldcat  44706  fldhmsubc  44708  crhmsubcALTV  44720  drhmsubcALTV  44722  drngcatALTV  44723  fldcatALTV  44724  fldhmsubcALTV  44726  zlmodzxznm  44906  ldepsnlinc  44917  nn0sumshdiglem2  45036  itcovalpclem1  45084  itcovalt2lem1  45089  rrx2xpref1o  45132  onsetrec  45237