Theorem rgen 3054

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3052

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

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

This theorem is referenced by:  ralel  3055  rgenw  3056  mprg  3058  mprgbir  3059  nrex  3065  rexlimivOLD  3171  rgen2  3185  r19.21be  3239  rexlimi  3246  rgen2a  3355  sbcth2  3864  r19.2zb  4476  unimax  4925  reusv2lem4  5376  wfisgOLD  6348  fnopab  6681  fmpti  7107  sorpssuni  7731  sorpssint  7732  onssmin  7791  tfis  7855  omssnlim  7881  finds  7897  finds2  7899  opabex3  7971  wfr3OLD  8357  seqomlem2  8470  findcard3  9295  findcard3OLD  9296  fifo  9449  fisupcl  9487  dfom3  9666  cantnfvalf  9684  frinsg  9770  rankf  9813  scottex  9904  cplem1  9908  harcard  9997  cardiun  10001  r0weon  10031  acnnum  10071  alephon  10088  alephsmo  10121  alephf1ALT  10122  alephfplem4  10126  dfac5lem4  10145  dfac5lem4OLD  10147  dfacacn  10161  kmlem1  10170  cflem  10264  cflemOLD  10265  cflecard  10272  cfsmolem  10289  fin23lem17  10357  hsmexlem4  10448  omina  10710  0tsk  10774  inar1  10794  wfgru  10835  reclem2pr  11067  nnssre  12249  nnsscn  12250  dfnn2  12258  dfnn3  12259  nnind  12263  nnsub  12289  dfuzi  12689  uzsupss  12961  cnref1o  13006  xrsupsslem  13328  xrinfmsslem  13329  xrsup0  13344  reltre  13362  rpltrp  13363  reltxrnmnf  13364  seqexw  14040  ser0f  14078  bccl  14345  hashkf  14355  hashbc  14476  wrdind  14745  01sqrexlem5  15270  sqrtf  15387  ackbijnn  15849  incexclem  15857  prodf1f  15913  eff2  16122  reeff1  16143  sqrt2irr  16272  prmind2  16709  3prm  16718  phisum  16815  pockthi  16932  infpn2  16938  prminf  16940  prmreclem2  16942  prmrec  16947  1arith  16952  1arith2  16953  vdwlem13  17018  ramz  17050  prmgap  17084  prmgaplcm  17085  prmgapprmo  17087  prmlem1a  17131  xpsff1o  17586  isacs1i  17674  dmaf  18067  cdaf  18068  coapm  18089  lublecllem  18375  smndex1mnd  18893  pwmnd  18920  pmtrdifel  19466  pmtrdifwrdel  19471  odf  19523  efgrelexlemb  19736  dprd2da  20030  rngmgpf  20122  mgpf  20213  prdscrngd  20287  crhmsubc  20647  drhmsubc  20746  drngcat  20747  fldcat  20748  fldhmsubc  20750  cnfld1  21361  cnfld1OLD  21362  cnsubglem  21388  cnmsubglem  21403  nn0srg  21410  rge0srg  21411  pzriprnglem4  21450  pzriprnglem9  21455  pzriprnglem14  21460  pmatcoe1fsupp  22644  isbasis3g  22892  basdif0  22896  distop  22938  mretopd  23035  2ndcsep  23402  refref  23456  kqf  23690  fbssfi  23780  filconn  23826  prdstmdd  24067  ustfilxp  24156  prdsxmslem2  24473  qdensere  24713  recld2  24759  isclmi0  25054  iscvsi  25085  ovolf  25440  dyadmax  25556  dveflem  25940  mdegxrf  26030  fta1  26273  vieta1  26277  aalioulem2  26298  taylfval  26323  pilem2  26419  pilem3  26420  recosf1o  26501  divlogrlim  26601  logcn  26613  ressatans  26901  leibpi  26909  ftalem3  27042  chtub  27180  2sqlem6  27391  2sqlem10  27396  2sqreulem4  27422  chtppilim  27443  pntpbnd1  27554  pntlem3  27577  padicabvf  27599  bdayfo  27646  nodense  27661  oldf  27822  scutfo  27873  addsfo  27947  negsf  28015  negsfo  28016  subsfo  28026  onsiso  28226  dfn0s2  28281  n0subs  28310  bdayn0sf1o  28316  dfnns2  28318  zs12bday  28400  axcontlem2  28949  nbgrnself  29343  vtxdginducedm1  29528  isgrpoi  30484  isvciOLD  30566  cnidOLD  30568  isnvi  30599  ipasslem8  30823  hilid  31147  hlimf  31223  shsspwh  31232  pjrni  31688  pjmf1  31702  df0op2  31738  dfiop2  31739  hoaddcomi  31758  hoaddassi  31762  hocadddiri  31765  hocsubdiri  31766  hoaddridi  31772  ho0coi  31774  hoid1i  31775  hoid1ri  31776  honegsubi  31782  hoddii  31975  lnopunilem2  31997  elunop2  31999  lnophm  32005  imaelshi  32044  cnlnadjlem8  32060  pjnmopi  32134  pjsdii  32141  pjddii  32142  pjtoi  32165  chirred  32381  nnindf  32803  nn0min  32804  wrdt2ind  32934  zringfrac  33574  ccfldsrarelvec  33717  constrconj  33784  2sqr3minply  33819  cos9thpiminply  33827  esum2d  34129  dmvlsiga  34165  volmeas  34267  ddemeas  34272  sxbrsigalem3  34309  coinfliprv  34520  ballotlem7  34573  signsw0glem  34590  rpsqrtcn  34630  tgoldbachgt  34700  bnj580  34949  bnj1384  35068  bnj1497  35096  kur14lem9  35241  sat1el2xp  35406  msrf  35569  dfon2lem7  35812  fobigcup  35923  nn0prpwlem  36345  topmeet  36387  onsucsuccmpi  36466  taupilemrplb  37343  relowlssretop  37386  ptrecube  37649  poimirlem27  37676  heicant  37684  mblfinlem1  37686  volsupnfl  37694  dvtan  37699  itg2addnc  37703  indexa  37762  sstotbnd2  37803  heiborlem7  37846  atpsubN  39777  idldil  40138  cdleme50ldil  40572  mzpclall  42725  dgraaf  43146  arearect  43214  areaquad  43215  onintunirab  43226  onsupuni  43228  infordmin  43531  omiscard  43542  clsk1indlem2  44041  clsk1indlem4  44043  mnuunid  44276  mnurndlem1  44280  prmunb2  44310  radcnvrat  44313  trwf  44959  rankrelp  44960  wfac8prim  45002  unirnmapsn  45218  ssmapsn  45220  upbdrech  45314  supminfxr  45471  supminfxr2  45476  supminfxrrnmpt  45478  rexanuz2nf  45499  fsumiunss  45584  resincncf  45884  dmvolss  45994  volioof  45996  stoweidlem57  46066  wallispilem3  46076  stirlinglem13  46095  dirkertrigeqlem3  46109  fourierdlem62  46177  salexct  46343  salexct3  46351  salgencntex  46352  salgensscntex  46353  gsumge0cl  46380  0ome  46538  icoresmbl  46552  hoidmv1le  46603  smflimlem1  46780  smfpimbor1lem2  46808  smfliminflem  46839  natlocalincr  46885  ralndv1  47114  fmtno4prm  47569  31prm  47591  tgoldbach  47811  gpg5grlic  48073  nn0mnd  48134  2zlidl  48195  2zrngagrp  48204  2zrngnmlid  48210  crhmsubcALTV  48282  drhmsubcALTV  48284  drngcatALTV  48285  fldcatALTV  48286  fldhmsubcALTV  48288  zlmodzxznm  48453  ldepsnlinc  48464  nn0sumshdiglem2  48582  itcovalpclem1  48630  itcovalt2lem1  48635  rrx2xpref1o  48678  slotresfo  48853  basresposfo  48932  setc2othin  49332  setcsnterm  49355  onsetrec  49552