Theorem rgen 3081

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∀wral 3079

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

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

This theorem is referenced by:  ralel  3082  rgenw  3083  mprg  3085  mprgbir  3086  nrex  3093  rgen2  3205  r19.21be  3258  rexlimi  3265  rgen2a  3360  sbcth2  3838  unimax  4911  reusv2lem4  5374  fnopab  6675  fmpti  7109  sorpssuni  7731  sorpssint  7732  onssmin  7792  tfis  7852  omssnlim  7878  finds  7894  finds2  7896  opabex3  7965  seqomlem2  8439  findcard3  9244  fifo  9393  fisupcl  9431  dfom3  9617  cantnfvalf  9635  frinsg  9724  rankf  9767  scottex  9860  cplem1  9876  harcard  9965  cardiun  9969  r0weon  9997  acnnum  10037  alephon  10054  alephsmo  10087  alephf1ALT  10088  alephfplem4  10092  dfac5lem4  10111  dfacacn  10126  kmlem1  10135  cflem  10229  cflemOLD  10230  cflecard  10237  cfsmolem  10255  fin23lem17  10323  hsmexlem4  10414  omina  10677  0tsk  10741  inar1  10761  wfgru  10802  reclem2pr  11034  nnssre  12238  nnsscn  12239  dfnn2  12247  dfnn3  12248  nnind  12252  nnsub  12281  dfuzi  12688  uzsupss  12965  cnref1o  13010  xrsupsslem  13334  xrinfmsslem  13335  xrsup0  13350  reltre  13368  rpltrp  13369  reltxrnmnf  13370  seqexw  14055  ser0f  14093  bccl  14360  hashkf  14370  hashbc  14492  wrdind  14761  sgnrn  15137  01sqrexlem5  15299  sqrtf  15417  ackbijnn  15884  incexclem  15892  prodf1f  15948  eff2  16156  reeff1  16177  sqrt2irr  16306  prmind2  16744  3prm  16753  phisum  16851  pockthi  16968  infpn2  16974  prminf  16976  prmreclem2  16978  prmrec  16983  1arith  16988  1arith2  16989  vdwlem13  17054  ramz  17086  prmgap  17120  prmgaplcm  17121  prmgapprmo  17123  prmlem1a  17167  xpsff1o  17622  isacs1i  17714  dmaf  18107  cdaf  18108  coapm  18129  lublecllem  18415  chninf  18692  ex-chn1  18694  ex-chn2  18695  smndex1mnd  18973  pwmnd  19000  pmtrdifel  19551  pmtrdifwrdel  19556  odf  19608  efgrelexlemb  19821  dprd2da  20115  rngmgpf  20236  mgpf  20331  prdscrngd  20404  crhmsubc  20768  drhmsubc  20865  drngcat  20866  fldcat  20867  fldhmsubc  20869  cnfld1  21528  cnsubglem  21547  cnmsubglem  21561  nn0srg  21568  rge0srg  21569  pzriprnglem4  21615  pzriprnglem9  21620  pzriprnglem14  21625  pmatcoe1fsupp  22839  isbasis3g  23087  basdif0  23091  distop  23133  mretopd  23230  2ndcsep  23597  refref  23651  kqf  23885  fbssfi  23975  filconn  24021  prdstmdd  24262  ustfilxp  24351  prdsxmslem2  24667  qdensere  24907  recld2  24953  isclmi0  25238  iscvsi  25269  ovolf  25622  dyadmax  25738  dveflem  26119  mdegxrf  26206  fta1  26450  vieta1  26454  aalioulem2  26475  taylfval  26500  pilem2  26593  pilem3  26594  recosf1o  26678  divlogrlim  26778  logcn  26790  ressatans  27077  leibpi  27085  ftalem3  27217  chtub  27354  2sqlem6  27565  2sqlem10  27570  2sqreulem4  27596  chtppilim  27617  pntpbnd1  27728  pntlem3  27751  padicabvf  27773  bdayfo  27819  nodense  27834  oldf  28008  cutsfo  28076  addsfo  28154  negsf  28223  negsfo  28224  subsfo  28236  oniso  28442  dfn0s2  28503  n0subs  28534  bdayn0sf1o  28541  dfnns2  28543  zsoring  28580  bdaypw2n0bndlem  28634  bdayfinbndlem2  28639  z12zsodd  28653  axcontlem2  29293  nbgrnself  29687  vtxdginducedm1  29871  isgrpoi  30828  isvciOLD  30910  cnidOLD  30912  isnvi  30943  ipasslem8  31167  hilid  31491  hlimf  31567  shsspwh  31576  pjrni  32032  pjmf1  32046  df0op2  32082  dfiop2  32083  hoaddcomi  32102  hoaddassi  32106  hocadddiri  32109  hocsubdiri  32110  hoaddridi  32116  ho0coi  32118  hoid1i  32119  hoid1ri  32120  honegsubi  32126  hoddii  32319  lnopunilem2  32341  elunop2  32343  lnophm  32349  imaelshi  32388  cnlnadjlem8  32404  pjnmopi  32478  pjsdii  32485  pjddii  32486  pjtoi  32509  chirred  32725  nnindf  33142  nn0min  33143  wrdt2ind  33251  zringfrac  33822  ccfldsrarelvec  34039  constrconj  34113  2sqr3minply  34148  cos9thpiminply  34156  esum2d  34461  dmvlsiga  34497  volmeas  34599  ddemeas  34604  sxbrsigalem3  34640  coinfliprv  34851  ballotlem7  34904  signsw0glem  34918  rpsqrtcn  34958  tgoldbachgt  35028  bnj580  35279  bnj1384  35398  bnj1497  35426  rankfo  35483  fineqvnttrclse  35515  onvf1odlem1  35565  kur14lem9  35684  sat1el2xp  35849  msrf  36012  dfon2lem7  36257  fobigcup  36368  nn0prpwlem  36811  topmeet  36853  onsucsuccmpi  36932  dfttc4lem2  37018  taupilemrplb  37942  relowlssretop  37987  ptrecube  38249  poimirlem27  38276  heicant  38284  mblfinlem1  38286  volsupnfl  38294  dvtan  38299  itg2addnc  38303  indexa  38362  sstotbnd2  38403  heiborlem7  38446  disjimeceqim  39431  atpsubN  40505  idldil  40866  cdleme50ldil  41300  mzpclall  43438  dgraaf  43854  arearect  43922  areaquad  43923  onintunirab  43934  onsupuni  43936  infordmin  44238  omiscard  44249  clsk1indlem2  44748  clsk1indlem4  44750  mnuunid  44967  mnurndlem1  44971  prmunb2  45001  radcnvrat  45004  trwf  45648  rankrelp  45649  wfac8prim  45691  unirnmapsn  45910  ssmapsn  45912  upbdrech  46004  supminfxr  46158  supminfxr2  46163  supminfxrrnmpt  46165  rexanuz2nf  46186  fsumiunss  46271  resincncf  46569  dmvolss  46679  volioof  46681  stoweidlem57  46751  wallispilem3  46761  stirlinglem13  46780  dirkertrigeqlem3  46794  fourierdlem62  46862  salexct  47028  salexct3  47036  salgencntex  47037  salgensscntex  47038  gsumge0cl  47065  0ome  47223  icoresmbl  47237  hoidmv1le  47288  smflimlem1  47465  smfpimbor1lem2  47493  smfliminflem  47524  natlocalincr  47572  sinnpoly  47605  ralndv1  47819  fmtno4prm  48304  31prm  48326  tgoldbach  48559  gpg5grlim  48835  gpg5grlic  48836  nn0mnd  48921  2zlidl  48982  2zrngagrp  48991  2zrngnmlid  48997  crhmsubcALTV  49069  drhmsubcALTV  49071  drngcatALTV  49072  fldcatALTV  49073  fldhmsubcALTV  49075  zlmodzxznm  49254  ldepsnlinc  49265  nn0sumshdiglem2  49379  itcovalpclem1  49427  itcovalt2lem1  49432  rrx2xpref1o  49475  slotresfo  49654  basresposfo  49733  oppff1  49903  setc2othin  50221  setcsnterm  50245  onsetrec  50463