Theorem rgen 3077

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∀wral 3075

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

This theorem depends on definitions:  df-bi 209  df-ral 3076

This theorem is referenced by:  ralel  3078  rgenw  3079  mprg  3081  mprgbir  3082  nrex  3089  rgen2  3201  r19.21be  3254  rexlimi  3261  rgen2a  3357  sbcth2  3837  unimax  4902  reusv2lem4  5357  fnopab  6655  fmpti  7089  sorpssuni  7711  sorpssint  7712  onssmin  7771  tfis  7831  omssnlim  7857  finds  7873  finds2  7875  opabex3  7944  seqomlem2  8417  findcard3  9223  fifo  9375  fisupcl  9413  dfom3  9599  cantnfvalf  9617  frinsg  9706  rankf  9749  scottex  9840  cplem1  9844  harcard  9933  cardiun  9937  r0weon  9965  acnnum  10005  alephon  10022  alephsmo  10055  alephf1ALT  10056  alephfplem4  10060  dfac5lem4  10079  dfac5lem4OLD  10081  dfacacn  10095  kmlem1  10104  cflem  10198  cflemOLD  10199  cflecard  10206  cfsmolem  10224  fin23lem17  10292  hsmexlem4  10383  omina  10646  0tsk  10710  inar1  10730  wfgru  10771  reclem2pr  11003  nnssre  12211  nnsscn  12212  dfnn2  12220  dfnn3  12221  nnind  12225  nnsub  12254  dfuzi  12661  uzsupss  12938  cnref1o  12983  xrsupsslem  13307  xrinfmsslem  13308  xrsup0  13323  reltre  13341  rpltrp  13342  reltxrnmnf  13343  seqexw  14027  ser0f  14065  bccl  14332  hashkf  14342  hashbc  14463  wrdind  14732  01sqrexlem5  15256  sqrtf  15374  ackbijnn  15841  incexclem  15849  prodf1f  15905  eff2  16114  reeff1  16135  sqrt2irr  16264  prmind2  16702  3prm  16711  phisum  16809  pockthi  16926  infpn2  16932  prminf  16934  prmreclem2  16936  prmrec  16941  1arith  16946  1arith2  16947  vdwlem13  17012  ramz  17044  prmgap  17078  prmgaplcm  17079  prmgapprmo  17081  prmlem1a  17125  xpsff1o  17580  isacs1i  17672  dmaf  18065  cdaf  18066  coapm  18087  lublecllem  18373  chninf  18650  ex-chn1  18652  ex-chn2  18653  smndex1mnd  18930  pwmnd  18957  pmtrdifel  19503  pmtrdifwrdel  19508  odf  19560  efgrelexlemb  19773  dprd2da  20067  rngmgpf  20186  mgpf  20277  prdscrngd  20349  crhmsubc  20711  drhmsubc  20810  drngcat  20811  fldcat  20812  fldhmsubc  20814  cnfld1  21429  cnsubglem  21448  cnmsubglem  21462  nn0srg  21469  rge0srg  21470  pzriprnglem4  21516  pzriprnglem9  21521  pzriprnglem14  21526  pmatcoe1fsupp  22741  isbasis3g  22989  basdif0  22993  distop  23035  mretopd  23132  2ndcsep  23499  refref  23553  kqf  23787  fbssfi  23877  filconn  23923  prdstmdd  24164  ustfilxp  24253  prdsxmslem2  24569  qdensere  24809  recld2  24855  isclmi0  25140  iscvsi  25171  ovolf  25524  dyadmax  25640  dveflem  26021  mdegxrf  26108  fta1  26349  vieta1  26353  aalioulem2  26374  taylfval  26399  pilem2  26492  pilem3  26493  recosf1o  26577  divlogrlim  26677  logcn  26689  ressatans  26976  leibpi  26984  ftalem3  27116  chtub  27253  2sqlem6  27464  2sqlem10  27469  2sqreulem4  27495  chtppilim  27516  pntpbnd1  27627  pntlem3  27650  padicabvf  27672  bdayfo  27718  nodense  27733  oldf  27907  cutsfo  27975  addsfo  28053  negsf  28122  negsfo  28123  subsfo  28135  oniso  28341  dfn0s2  28402  n0subs  28433  bdayn0sf1o  28440  dfnns2  28442  zsoring  28479  bdaypw2n0bndlem  28533  bdayfinbndlem2  28538  z12zsodd  28552  axcontlem2  29112  nbgrnself  29506  vtxdginducedm1  29690  isgrpoi  30647  isvciOLD  30729  cnidOLD  30731  isnvi  30762  ipasslem8  30986  hilid  31310  hlimf  31386  shsspwh  31395  pjrni  31851  pjmf1  31865  df0op2  31901  dfiop2  31902  hoaddcomi  31921  hoaddassi  31925  hocadddiri  31928  hocsubdiri  31929  hoaddridi  31935  ho0coi  31937  hoid1i  31938  hoid1ri  31939  honegsubi  31945  hoddii  32138  lnopunilem2  32160  elunop2  32162  lnophm  32168  imaelshi  32207  cnlnadjlem8  32223  pjnmopi  32297  pjsdii  32304  pjddii  32305  pjtoi  32328  chirred  32544  nnindf  32972  nn0min  32973  wrdt2ind  33092  zringfrac  33711  ccfldsrarelvec  33929  constrconj  34003  2sqr3minply  34038  cos9thpiminply  34046  esum2d  34351  dmvlsiga  34387  volmeas  34489  ddemeas  34494  sxbrsigalem3  34530  coinfliprv  34741  ballotlem7  34794  signsw0glem  34811  rpsqrtcn  34851  tgoldbachgt  34921  bnj580  35172  bnj1384  35291  bnj1497  35319  fineqvnttrclse  35384  onvf1odlem1  35410  kur14lem9  35528  sat1el2xp  35693  msrf  35856  dfon2lem7  36101  fobigcup  36212  nn0prpwlem  36646  topmeet  36688  onsucsuccmpi  36767  dfttc4lem2  36853  taupilemrplb  37776  relowlssretop  37821  ptrecube  38083  poimirlem27  38110  heicant  38118  mblfinlem1  38120  volsupnfl  38128  dvtan  38133  itg2addnc  38137  indexa  38196  sstotbnd2  38237  heiborlem7  38280  disjimeceqim  39267  atpsubN  40341  idldil  40702  cdleme50ldil  41136  mzpclall  43272  dgraaf  43688  arearect  43756  areaquad  43757  onintunirab  43768  onsupuni  43770  infordmin  44072  omiscard  44083  clsk1indlem2  44582  clsk1indlem4  44584  mnuunid  44817  mnurndlem1  44821  prmunb2  44851  radcnvrat  44854  trwf  45499  rankrelp  45500  wfac8prim  45542  unirnmapsn  45754  ssmapsn  45756  upbdrech  45848  supminfxr  46002  supminfxr2  46007  supminfxrrnmpt  46009  rexanuz2nf  46030  fsumiunss  46115  resincncf  46413  dmvolss  46523  volioof  46525  stoweidlem57  46595  wallispilem3  46605  stirlinglem13  46624  dirkertrigeqlem3  46638  fourierdlem62  46706  salexct  46872  salexct3  46880  salgencntex  46881  salgensscntex  46882  gsumge0cl  46909  0ome  47067  icoresmbl  47081  hoidmv1le  47132  smflimlem1  47309  smfpimbor1lem2  47337  smfliminflem  47368  natlocalincr  47416  sinnpoly  47449  ralndv1  47663  fmtno4prm  48148  31prm  48170  tgoldbach  48403  gpg5grlim  48679  gpg5grlic  48680  nn0mnd  48765  2zlidl  48826  2zrngagrp  48835  2zrngnmlid  48841  crhmsubcALTV  48913  drhmsubcALTV  48915  drngcatALTV  48916  fldcatALTV  48917  fldhmsubcALTV  48919  zlmodzxznm  49083  ldepsnlinc  49094  nn0sumshdiglem2  49208  itcovalpclem1  49256  itcovalt2lem1  49261  rrx2xpref1o  49304  slotresfo  49484  basresposfo  49563  oppff1  49733  setc2othin  50051  setcsnterm  50075  onsetrec  50293