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 1822	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

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

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

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  3361  sbcth2  3840  unimax  4906  reusv2lem4  5363  fnopab  6663  fmpti  7097  sorpssuni  7719  sorpssint  7720  onssmin  7779  tfis  7839  omssnlim  7865  finds  7881  finds2  7883  opabex3  7952  seqomlem2  8426  findcard3  9231  fifo  9380  fisupcl  9418  dfom3  9604  cantnfvalf  9622  frinsg  9711  rankf  9754  scottex  9847  cplem1  9863  harcard  9952  cardiun  9956  r0weon  9984  acnnum  10024  alephon  10041  alephsmo  10074  alephf1ALT  10075  alephfplem4  10079  dfac5lem4  10098  dfacacn  10113  kmlem1  10122  cflem  10216  cflemOLD  10217  cflecard  10224  cfsmolem  10242  fin23lem17  10310  hsmexlem4  10401  omina  10664  0tsk  10728  inar1  10748  wfgru  10789  reclem2pr  11021  nnssre  12228  nnsscn  12229  dfnn2  12237  dfnn3  12238  nnind  12242  nnsub  12271  dfuzi  12678  uzsupss  12955  cnref1o  13000  xrsupsslem  13324  xrinfmsslem  13325  xrsup0  13340  reltre  13358  rpltrp  13359  reltxrnmnf  13360  seqexw  14044  ser0f  14082  bccl  14349  hashkf  14359  hashbc  14480  wrdind  14749  sgnrn  15125  01sqrexlem5  15287  sqrtf  15405  ackbijnn  15872  incexclem  15880  prodf1f  15936  eff2  16145  reeff1  16166  sqrt2irr  16295  prmind2  16733  3prm  16742  phisum  16840  pockthi  16957  infpn2  16963  prminf  16965  prmreclem2  16967  prmrec  16972  1arith  16977  1arith2  16978  vdwlem13  17043  ramz  17075  prmgap  17109  prmgaplcm  17110  prmgapprmo  17112  prmlem1a  17156  xpsff1o  17611  isacs1i  17703  dmaf  18096  cdaf  18097  coapm  18118  lublecllem  18404  chninf  18681  ex-chn1  18683  ex-chn2  18684  smndex1mnd  18962  pwmnd  18989  pmtrdifel  19541  pmtrdifwrdel  19546  odf  19598  efgrelexlemb  19811  dprd2da  20105  rngmgpf  20226  mgpf  20321  prdscrngd  20394  crhmsubc  20758  drhmsubc  20853  drngcat  20854  fldcat  20855  fldhmsubc  20857  cnfld1  21507  cnsubglem  21526  cnmsubglem  21540  nn0srg  21547  rge0srg  21548  pzriprnglem4  21594  pzriprnglem9  21599  pzriprnglem14  21604  pmatcoe1fsupp  22819  isbasis3g  23067  basdif0  23071  distop  23113  mretopd  23210  2ndcsep  23577  refref  23631  kqf  23865  fbssfi  23955  filconn  24001  prdstmdd  24242  ustfilxp  24331  prdsxmslem2  24647  qdensere  24887  recld2  24933  isclmi0  25218  iscvsi  25249  ovolf  25602  dyadmax  25718  dveflem  26099  mdegxrf  26186  fta1  26430  vieta1  26434  aalioulem2  26455  taylfval  26480  pilem2  26573  pilem3  26574  recosf1o  26658  divlogrlim  26758  logcn  26770  ressatans  27057  leibpi  27065  ftalem3  27197  chtub  27334  2sqlem6  27545  2sqlem10  27550  2sqreulem4  27576  chtppilim  27597  pntpbnd1  27708  pntlem3  27731  padicabvf  27753  bdayfo  27799  nodense  27814  oldf  27988  cutsfo  28056  addsfo  28134  negsf  28203  negsfo  28204  subsfo  28216  oniso  28422  dfn0s2  28483  n0subs  28514  bdayn0sf1o  28521  dfnns2  28523  zsoring  28560  bdaypw2n0bndlem  28614  bdayfinbndlem2  28619  z12zsodd  28633  axcontlem2  29224  nbgrnself  29618  vtxdginducedm1  29802  isgrpoi  30759  isvciOLD  30841  cnidOLD  30843  isnvi  30874  ipasslem8  31098  hilid  31422  hlimf  31498  shsspwh  31507  pjrni  31963  pjmf1  31977  df0op2  32013  dfiop2  32014  hoaddcomi  32033  hoaddassi  32037  hocadddiri  32040  hocsubdiri  32041  hoaddridi  32047  ho0coi  32049  hoid1i  32050  hoid1ri  32051  honegsubi  32057  hoddii  32250  lnopunilem2  32272  elunop2  32274  lnophm  32280  imaelshi  32319  cnlnadjlem8  32335  pjnmopi  32409  pjsdii  32416  pjddii  32417  pjtoi  32440  chirred  32656  nnindf  33077  nn0min  33078  wrdt2ind  33186  zringfrac  33761  ccfldsrarelvec  33978  constrconj  34052  2sqr3minply  34087  cos9thpiminply  34095  esum2d  34400  dmvlsiga  34436  volmeas  34538  ddemeas  34543  sxbrsigalem3  34579  coinfliprv  34790  ballotlem7  34843  signsw0glem  34857  rpsqrtcn  34897  tgoldbachgt  34967  bnj580  35218  bnj1384  35337  bnj1497  35365  fineqvnttrclse  35432  onvf1odlem1  35458  kur14lem9  35577  sat1el2xp  35742  msrf  35905  dfon2lem7  36150  fobigcup  36261  nn0prpwlem  36695  topmeet  36737  onsucsuccmpi  36816  dfttc4lem2  36902  taupilemrplb  37824  relowlssretop  37869  ptrecube  38131  poimirlem27  38158  heicant  38166  mblfinlem1  38168  volsupnfl  38176  dvtan  38181  itg2addnc  38185  indexa  38244  sstotbnd2  38285  heiborlem7  38328  disjimeceqim  39315  atpsubN  40389  idldil  40750  cdleme50ldil  41184  mzpclall  43320  dgraaf  43736  arearect  43804  areaquad  43805  onintunirab  43816  onsupuni  43818  infordmin  44120  omiscard  44131  clsk1indlem2  44630  clsk1indlem4  44632  mnuunid  44851  mnurndlem1  44855  prmunb2  44885  radcnvrat  44888  trwf  45533  rankrelp  45534  wfac8prim  45576  unirnmapsn  45788  ssmapsn  45790  upbdrech  45882  supminfxr  46036  supminfxr2  46041  supminfxrrnmpt  46043  rexanuz2nf  46064  fsumiunss  46149  resincncf  46447  dmvolss  46557  volioof  46559  stoweidlem57  46629  wallispilem3  46639  stirlinglem13  46658  dirkertrigeqlem3  46672  fourierdlem62  46740  salexct  46906  salexct3  46914  salgencntex  46915  salgensscntex  46916  gsumge0cl  46943  0ome  47101  icoresmbl  47115  hoidmv1le  47166  smflimlem1  47343  smfpimbor1lem2  47371  smfliminflem  47402  natlocalincr  47450  sinnpoly  47483  ralndv1  47697  fmtno4prm  48182  31prm  48204  tgoldbach  48437  gpg5grlim  48713  gpg5grlic  48714  nn0mnd  48799  2zlidl  48860  2zrngagrp  48869  2zrngnmlid  48875  crhmsubcALTV  48947  drhmsubcALTV  48949  drngcatALTV  48950  fldcatALTV  48951  fldhmsubcALTV  48953  zlmodzxznm  49128  ldepsnlinc  49139  nn0sumshdiglem2  49253  itcovalpclem1  49301  itcovalt2lem1  49306  rrx2xpref1o  49349  slotresfo  49528  basresposfo  49607  oppff1  49777  setc2othin  50095  setcsnterm  50119  onsetrec  50337