Theorem rgen 3052

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

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

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

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

This theorem is referenced by:  ralel  3053  rgenw  3054  mprg  3056  mprgbir  3057  nrex  3063  rexlimivOLD  3172  rgen2  3186  r19.21be  3239  rexlimi  3246  rgen2a  3355  sbcth2  3866  r19.2zb  4478  unimax  4926  mpteq1OLD  5218  mpteq2iaOLD  5228  reusv2lem4  5383  wfisgOLD  6356  fnopab  6687  fmpti  7113  sorpssuni  7735  sorpssint  7736  onssmin  7795  tfis  7859  omssnlim  7885  finds  7901  finds2  7903  opabex3  7975  wfr3OLD  8361  seqomlem2  8474  findcard3  9301  findcard3OLD  9302  fifo  9455  fisupcl  9492  dfom3  9670  cantnfvalf  9688  frinsg  9774  rankf  9817  scottex  9908  cplem1  9912  harcard  10001  cardiun  10005  r0weon  10035  acnnum  10075  alephon  10092  alephsmo  10125  alephf1ALT  10126  alephfplem4  10130  dfac5lem4  10149  dfac5lem4OLD  10151  dfacacn  10165  kmlem1  10174  cflem  10268  cflemOLD  10269  cflecard  10276  cfsmolem  10293  fin23lem17  10361  hsmexlem4  10452  omina  10714  0tsk  10778  inar1  10798  wfgru  10839  reclem2pr  11071  nnssre  12253  nnsscn  12254  dfnn2  12262  dfnn3  12263  nnind  12267  nnsub  12293  dfuzi  12693  uzsupss  12965  cnref1o  13010  xrsupsslem  13332  xrinfmsslem  13333  xrsup0  13348  reltre  13365  rpltrp  13366  reltxrnmnf  13367  seqexw  14041  ser0f  14079  bccl  14344  hashkf  14354  hashbc  14475  wrdind  14743  01sqrexlem5  15268  sqrtf  15385  ackbijnn  15847  incexclem  15855  prodf1f  15911  eff2  16118  reeff1  16139  sqrt2irr  16268  prmind2  16705  3prm  16714  phisum  16811  pockthi  16928  infpn2  16934  prminf  16936  prmreclem2  16938  prmrec  16943  1arith  16948  1arith2  16949  vdwlem13  17014  ramz  17046  prmgap  17080  prmgaplcm  17081  prmgapprmo  17083  prmlem1a  17127  xpsff1o  17588  isacs1i  17676  dmaf  18070  cdaf  18071  coapm  18092  lublecllem  18379  smndex1mnd  18897  pwmnd  18924  pmtrdifel  19471  pmtrdifwrdel  19476  odf  19528  efgrelexlemb  19741  dprd2da  20035  rngmgpf  20127  mgpf  20218  prdscrngd  20292  crhmsubc  20655  drhmsubc  20755  drngcat  20756  fldcat  20757  fldhmsubc  20759  cnfld1  21373  cnfld1OLD  21374  cnsubglem  21400  cnmsubglem  21415  nn0srg  21422  rge0srg  21423  pzriprnglem4  21462  pzriprnglem9  21467  pzriprnglem14  21472  pmatcoe1fsupp  22674  isbasis3g  22922  basdif0  22926  distop  22968  mretopd  23065  2ndcsep  23432  refref  23486  kqf  23720  fbssfi  23810  filconn  23856  prdstmdd  24097  ustfilxp  24186  prdsxmslem2  24505  qdensere  24745  recld2  24791  isclmi0  25086  iscvsi  25117  ovolf  25472  dyadmax  25588  dveflem  25972  mdegxrf  26062  fta1  26305  vieta1  26309  aalioulem2  26330  taylfval  26355  pilem2  26451  pilem3  26452  recosf1o  26532  divlogrlim  26632  logcn  26644  ressatans  26932  leibpi  26940  ftalem3  27073  chtub  27211  2sqlem6  27422  2sqlem10  27427  2sqreulem4  27453  chtppilim  27474  pntpbnd1  27585  pntlem3  27608  padicabvf  27630  bdayfo  27677  nodense  27692  oldf  27851  scutfo  27897  addsfo  27971  negsf  28039  negsfo  28040  subsfo  28050  dfn0s2  28291  n0subs  28315  dfnns2  28317  zs12bday  28379  axcontlem2  28929  nbgrnself  29323  vtxdginducedm1  29508  isgrpoi  30464  isvciOLD  30546  cnidOLD  30548  isnvi  30579  ipasslem8  30803  hilid  31127  hlimf  31203  shsspwh  31212  pjrni  31668  pjmf1  31682  df0op2  31718  dfiop2  31719  hoaddcomi  31738  hoaddassi  31742  hocadddiri  31745  hocsubdiri  31746  hoaddridi  31752  ho0coi  31754  hoid1i  31755  hoid1ri  31756  honegsubi  31762  hoddii  31955  lnopunilem2  31977  elunop2  31979  lnophm  31985  imaelshi  32024  cnlnadjlem8  32040  pjnmopi  32114  pjsdii  32121  pjddii  32122  pjtoi  32145  chirred  32361  nnindf  32768  nn0min  32769  wrdt2ind  32885  zringfrac  33523  ccfldsrarelvec  33662  constrconj  33727  2sqr3minply  33732  esum2d  34035  dmvlsiga  34071  volmeas  34173  ddemeas  34178  sxbrsigalem3  34215  coinfliprv  34426  ballotlem7  34479  signsw0glem  34509  rpsqrtcn  34549  tgoldbachgt  34619  bnj580  34868  bnj1384  34987  bnj1497  35015  kur14lem9  35160  sat1el2xp  35325  msrf  35488  dfon2lem7  35731  fobigcup  35842  nn0prpwlem  36264  topmeet  36306  onsucsuccmpi  36385  taupilemrplb  37262  relowlssretop  37305  ptrecube  37568  poimirlem27  37595  heicant  37603  mblfinlem1  37605  volsupnfl  37613  dvtan  37618  itg2addnc  37622  indexa  37681  sstotbnd2  37722  heiborlem7  37765  atpsubN  39696  idldil  40057  cdleme50ldil  40491  mzpclall  42683  dgraaf  43104  arearect  43172  areaquad  43173  onintunirab  43184  onsupuni  43186  infordmin  43490  omiscard  43501  clsk1indlem2  44000  clsk1indlem4  44002  mnuunid  44241  mnurndlem1  44245  prmunb2  44275  radcnvrat  44278  trwf  44921  rankrelp  44922  wfac8prim  44964  unirnmapsn  45164  ssmapsn  45166  upbdrech  45262  supminfxr  45420  supminfxr2  45425  supminfxrrnmpt  45427  rexanuz2nf  45448  fsumiunss  45535  resincncf  45835  dmvolss  45945  volioof  45947  stoweidlem57  46017  wallispilem3  46027  stirlinglem13  46046  dirkertrigeqlem3  46060  fourierdlem62  46128  salexct  46294  salexct3  46302  salgencntex  46303  salgensscntex  46304  gsumge0cl  46331  0ome  46489  icoresmbl  46503  hoidmv1le  46554  smflimlem1  46731  smfpimbor1lem2  46759  smfliminflem  46790  natlocalincr  46836  ralndv1  47063  fmtno4prm  47508  31prm  47530  tgoldbach  47750  gpg5grlic  47993  nn0mnd  48041  2zlidl  48102  2zrngagrp  48111  2zrngnmlid  48117  crhmsubcALTV  48189  drhmsubcALTV  48191  drngcatALTV  48192  fldcatALTV  48193  fldhmsubcALTV  48195  zlmodzxznm  48360  ldepsnlinc  48371  nn0sumshdiglem2  48489  itcovalpclem1  48537  itcovalt2lem1  48542  rrx2xpref1o  48585  slotresfo  48744  basresposfo  48823  setc2othin  49079  setcsnterm  49102  onsetrec  49223