Theorem rgen 3084

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∀wral 3082

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ral 3083

This theorem is used by:  ralel  3085  rgenw  3086  mprg  3088  mprgbir  3089  nrex  3096  rgen2  3208  r19.21be  3261  rexlimi  3268  rgen2a  3363  sbcth2  3840  unimax  4915  reusv2lem4  5377  fnopab  6680  fmpti  7114  sorpssuni  7742  sorpssint  7743  onssmin  7800  tfis  7860  omssnlim  7886  finds  7902  finds2  7904  opabex3  7973  seqomlem2  8447  findcard3  9253  fifo  9402  fisupcl  9440  dfom3  9626  cantnfvalf  9644  frinsg  9733  rankf  9776  scottex  9872  scottexOLD  9873  cplem1  9889  cplem1OLD  9890  harcard  9983  cardiun  9987  r0weon  10015  acnnum  10055  alephon  10072  alephsmo  10105  alephf1ALT  10106  alephfplem4  10110  dfac5lem4  10129  dfacacn  10144  kmlem1  10153  cflem  10247  cflecard  10254  cfsmolem  10272  fin23lem17  10340  hsmexlem4  10431  omina  10694  0tsk  10758  inar1  10778  wfgru  10819  reclem2pr  11051  nnssre  12255  nnsscn  12256  dfnn2  12264  dfnn3  12265  nnind  12269  nnsub  12298  dfuzi  12705  uzsupss  12982  cnref1o  13027  xrsupsslem  13351  xrinfmsslem  13352  xrsup0  13367  reltre  13385  rpltrp  13386  reltxrnmnf  13387  seqexw  14073  ser0f  14111  bccl  14378  hashkf  14388  hashbc  14510  wrdind  14783  sgnrn  15161  01sqrexlem5  15323  sqrtf  15441  ackbijnn  15908  incexclem  15916  prodf1f  15972  eff2  16180  reeff1  16201  sqrt2irr  16330  prmind2  16768  3prm  16777  phisum  16875  pockthi  16992  infpn2  16998  prminf  17000  prmreclem2  17002  prmrec  17007  1arith  17012  1arith2  17013  vdwlem13  17078  ramz  17110  prmgap  17144  prmgaplcm  17145  prmgapprmo  17147  prmlem1a  17191  xpsff1o  17646  isacs1i  17738  dmaf  18131  cdaf  18132  coapm  18153  lublecllem  18439  chninf  18716  ex-chn1  18718  ex-chn2  18719  smndex1mnd  19003  pwmnd  19030  pmtrdifel  19581  pmtrdifwrdel  19586  odf  19638  efgrelexlemb  19851  dprd2da  20145  rngmgpf  20266  mgpf  20361  prdscrngd  20436  crhmsubc  20818  drhmsubc  20921  drngcat  20922  fldcat  20923  fldhmsubc  20925  cnfld1  21584  cnsubglem  21603  cnmsubglem  21617  nn0srg  21624  rge0srg  21625  pzriprnglem4  21671  pzriprnglem9  21676  pzriprnglem14  21681  pmatcoe1fsupp  22895  isbasis3g  23143  basdif0  23147  distop  23189  mretopd  23286  2ndcsep  23653  refref  23707  kqf  23941  fbssfi  24031  filconn  24077  prdstmdd  24318  ustfilxp  24407  prdsxmslem2  24723  qdensere  24963  recld2  25009  isclmi0  25294  iscvsi  25325  ovolf  25678  dyadmax  25794  dveflem  26175  mdegxrf  26262  fta1  26506  vieta1  26510  aalioulem2  26533  taylfval  26559  pilem2  26652  pilem3  26653  recosf1o  26737  divlogrlim  26837  logcn  26849  ressatans  27136  leibpi  27144  ftalem3  27276  chtub  27413  2sqlem6  27624  2sqlem10  27629  2sqreulem4  27655  chtppilim  27676  pntpbnd1  27787  pntlem3  27810  padicabvf  27832  bdayfo  27878  nodense  27893  oldf  28067  cutsfo  28135  addsfo  28213  negsf  28282  negsfo  28283  subsfo  28295  oniso  28501  dfn0s2  28562  n0subs  28593  bdayn0sf1o  28600  dfnns2  28602  zsoring  28639  bdaypw2n0bndlem  28693  bdayfinbndlem2  28698  z12zsodd  28712  axcontlem2  29352  nbgrnself  29746  vtxdginducedm1  29930  isgrpoi  30887  isvciOLD  30969  cnidOLD  30971  isnvi  31002  ipasslem8  31226  hilid  31550  hlimf  31626  shsspwh  31635  pjrni  32091  pjmf1  32105  df0op2  32141  dfiop2  32142  hoaddcomi  32161  hoaddassi  32165  hocadddiri  32168  hocsubdiri  32169  hoaddridi  32175  ho0coi  32177  hoid1i  32178  hoid1ri  32179  honegsubi  32185  hoddii  32378  lnopunilem2  32400  elunop2  32402  lnophm  32408  imaelshi  32447  cnlnadjlem8  32463  pjnmopi  32537  pjsdii  32544  pjddii  32545  pjtoi  32568  chirred  32784  nnindf  33201  nn0min  33202  wrdt2ind  33306  zringfrac  33875  ccfldsrarelvec  34092  constrconj  34166  2sqr3minply  34201  cos9thpiminply  34209  esum2d  34514  dmvlsiga  34550  volmeas  34652  ddemeas  34657  sxbrsigalem3  34693  coinfliprv  34904  ballotlem7  34957  signsw0glem  34971  rpsqrtcn  35011  tgoldbachgt  35081  bnj580  35332  bnj1384  35451  bnj1497  35479  rankfo  35529  fineqvnttrclse  35560  onvf1odlem1  35610  kur14lem9  35726  sat1el2xp  35891  msrf  36054  dfon2lem7  36299  fobigcup  36410  nn0prpwlem  36873  topmeet  36915  onsucsuccmpi  36994  dfttc4lem2  37080  taupilemrplb  38004  relowlssretop  38049  ptrecube  38311  poimirlem27  38338  heicant  38346  mblfinlem1  38348  volsupnfl  38356  dvtan  38361  itg2addnc  38365  indexa  38424  sstotbnd2  38465  heiborlem7  38508  disjimeceqim  39493  atpsubN  40567  idldil  40928  cdleme50ldil  41362  mzpclall  43498  dgraaf  43914  arearect  43982  areaquad  43983  onintunirab  43994  onsupuni  43996  infordmin  44298  omiscard  44309  clsk1indlem2  44808  clsk1indlem4  44810  mnuunid  45027  mnurndlem1  45031  prmunb2  45061  radcnvrat  45064  trwf  45708  rankrelp  45709  wfac8prim  45751  unirnmapsn  45970  ssmapsn  45972  upbdrech  46064  supminfxr  46218  supminfxr2  46223  supminfxrrnmpt  46225  rexanuz2nf  46246  fsumiunss  46331  resincncf  46629  dmvolss  46739  volioof  46741  stoweidlem57  46811  wallispilem3  46821  stirlinglem13  46840  dirkertrigeqlem3  46854  fourierdlem62  46922  salexct  47088  salexct3  47096  salgencntex  47097  salgensscntex  47098  gsumge0cl  47125  0ome  47283  icoresmbl  47297  hoidmv1le  47348  smflimlem1  47525  smfpimbor1lem2  47553  smfliminflem  47584  natlocalincr  47632  sinnpoly  47668  ralndv1  47882  fmtno4prm  48367  31prm  48389  tgoldbach  48622  gpg5grlim  48898  gpg5grlic  48899  nn0mnd  48984  2zlidl  49045  2zrngagrp  49054  2zrngnmlid  49060  crhmsubcALTV  49132  drhmsubcALTV  49134  drngcatALTV  49135  fldcatALTV  49136  fldhmsubcALTV  49138  zlmodzxznm  49317  ldepsnlinc  49328  nn0sumshdiglem2  49442  itcovalpclem1  49490  itcovalt2lem1  49495  rrx2xpref1o  49538  slotresfo  49717  basresposfo  49796  oppff1  49966  setc2othin  50284  setcsnterm  50308  onsetrec  50526