Theorem rgen 3063

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3053

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

This theorem depends on definitions:  df-bi 210  df-ral 3058

This theorem is referenced by:  ralel  3064  rgenw  3065  mprg  3067  mprgbir  3068  rgen2  3115  r19.21be  3121  rgen2a  3142  nrex  3178  rexlimiv  3189  rexlimi  3224  sbcth2  3773  r19.2zb  4379  ral0OLD  4400  unimax  4831  mpteq1  5115  mpteq2ia  5118  reusv2lem4  5265  wfisg  6158  fnopab  6469  fmpti  6880  sorpssuni  7470  sorpssint  7471  onssmin  7525  tfis  7582  omssnlim  7607  finds  7622  finds2  7624  opabex3  7686  wfr3  7997  seqomlem2  8109  findcard3  8828  fifo  8962  fisupcl  8999  dfom3  9176  cantnfvalf  9194  rankf  9289  scottex  9380  cplem1  9384  harcard  9473  cardiun  9477  r0weon  9505  acnnum  9545  alephon  9562  alephsmo  9595  alephf1ALT  9596  alephfplem4  9600  dfac5lem4  9619  dfacacn  9634  kmlem1  9643  cflem  9739  cflecard  9746  cfsmolem  9763  fin23lem17  9831  hsmexlem4  9922  omina  10184  0tsk  10248  inar1  10268  wfgru  10309  reclem2pr  10541  nnssre  11713  nnsscn  11714  dfnn2  11722  dfnn3  11723  nnind  11727  nnsub  11753  dfuzi  12147  uzsupss  12415  cnref1o  12460  xrsupsslem  12776  xrinfmsslem  12777  xrsup0  12792  reltre  12809  rpltrp  12810  reltxrnmnf  12811  seqexw  13469  ser0f  13508  bccl  13767  hashkf  13777  hashbc  13896  wrdind  14166  sqrlem5  14689  sqrtf  14806  ackbijnn  15269  incexclem  15277  prodf1f  15333  eff2  15537  reeff1  15558  sqrt2irr  15687  prmind2  16119  3prm  16128  phisum  16220  pockthi  16336  infpn2  16342  prminf  16344  prmreclem2  16346  prmrec  16351  1arith  16356  1arith2  16357  vdwlem13  16422  ramz  16454  prmgap  16488  prmgaplcm  16489  prmgapprmo  16491  prmlem1a  16536  xpsff1o  16936  isacs1i  17024  dmaf  17414  cdaf  17415  coapm  17436  lublecllem  17707  smndex1mnd  18184  pwmnd  18211  pmtrdifel  18719  pmtrdifwrdel  18724  odf  18776  efgrelexlemb  18987  dprd2da  19276  mgpf  19424  prdscrngd  19478  cnfld1  20235  cnsubglem  20259  cnmsubglem  20273  nn0srg  20280  rge0srg  20281  pmatcoe1fsupp  21445  isbasis3g  21693  basdif0  21697  distop  21739  mretopd  21836  2ndcsep  22203  refref  22257  kqf  22491  fbssfi  22581  filconn  22627  prdstmdd  22868  ustfilxp  22957  prdsxmslem2  23275  qdensere  23515  recld2  23559  isclmi0  23843  iscvsi  23874  ovolf  24227  dyadmax  24343  dveflem  24723  mdegxrf  24813  fta1  25048  vieta1  25052  aalioulem2  25073  taylfval  25098  pilem2  25191  pilem3  25192  recosf1o  25271  divlogrlim  25370  logcn  25382  ressatans  25664  leibpi  25672  ftalem3  25804  chtub  25940  2sqlem6  26151  2sqlem10  26156  2sqreulem4  26182  chtppilim  26203  pntpbnd1  26314  pntlem3  26337  padicabvf  26359  axcontlem2  26903  nbgrnself  27293  vtxdginducedm1  27477  isgrpoi  28425  isvciOLD  28507  cnidOLD  28509  isnvi  28540  ipasslem8  28764  hilid  29088  hlimf  29164  shsspwh  29173  pjrni  29629  pjmf1  29643  df0op2  29679  dfiop2  29680  hoaddcomi  29699  hoaddassi  29703  hocadddiri  29706  hocsubdiri  29707  hoaddid1i  29713  ho0coi  29715  hoid1i  29716  hoid1ri  29717  honegsubi  29723  hoddii  29916  lnopunilem2  29938  elunop2  29940  lnophm  29946  imaelshi  29985  cnlnadjlem8  30001  pjnmopi  30075  pjsdii  30082  pjddii  30083  pjtoi  30106  chirred  30322  nnindf  30700  nn0min  30701  wrdt2ind  30792  ccfldsrarelvec  31305  esum2d  31623  dmvlsiga  31659  volmeas  31761  ddemeas  31766  sxbrsigalem3  31801  coinfliprv  32011  ballotlem7  32064  signsw0glem  32094  rpsqrtcn  32135  tgoldbachgt  32205  bnj580  32456  bnj1384  32575  bnj1497  32603  kur14lem9  32739  sat1el2xp  32904  msrf  33067  dfon2lem7  33329  frinsg  33385  bdayfo  33513  nodense  33528  oldf  33674  scutfo  33714  fobigcup  33832  nn0prpwlem  34141  topmeet  34183  onsucsuccmpi  34262  taupilemrplb  35100  relowlssretop  35146  ptrecube  35389  poimirlem27  35416  heicant  35424  mblfinlem1  35426  volsupnfl  35434  dvtan  35439  itg2addnc  35443  indexa  35503  sstotbnd2  35544  heiborlem7  35587  atpsubN  37379  idldil  37740  cdleme50ldil  38174  mzpclall  40105  dgraaf  40528  arearect  40602  areaquad  40603  infordmin  40677  clsk1indlem2  41182  clsk1indlem4  41184  mnuunid  41421  mnurndlem1  41425  prmunb2  41451  radcnvrat  41454  unirnmapsn  42276  ssmapsn  42278  upbdrech  42366  supminfxr  42528  supminfxr2  42533  supminfxrrnmpt  42535  fsumiunss  42642  resincncf  42942  dmvolss  43052  volioof  43054  stoweidlem57  43124  wallispilem3  43134  stirlinglem13  43153  dirkertrigeqlem3  43167  fourierdlem62  43235  salexct  43399  salexct3  43407  salgencntex  43408  salgensscntex  43409  gsumge0cl  43435  0ome  43593  icoresmbl  43607  hoidmv1le  43658  smflimlem1  43829  smfpimbor1lem2  43856  smfliminflem  43886  ralndv1  44114  fmtno4prm  44545  31prm  44567  tgoldbach  44787  nn0mnd  44891  2zlidl  45010  2zrngagrp  45019  2zrngnmlid  45025  crhmsubc  45154  drhmsubc  45156  drngcat  45157  fldcat  45158  fldhmsubc  45160  crhmsubcALTV  45172  drhmsubcALTV  45174  drngcatALTV  45175  fldcatALTV  45176  fldhmsubcALTV  45178  zlmodzxznm  45356  ldepsnlinc  45367  nn0sumshdiglem2  45486  itcovalpclem1  45534  itcovalt2lem1  45539  rrx2xpref1o  45582  setc2othin  45785  onsetrec  45850