Theorem rgen 2906

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

Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896

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

This theorem depends on definitions:  df-bi 196  df-ral 2901

This theorem is referenced by:  ralel  2907  rgenw  2908  mprg  2910  mprgbir  2911  r19.21be  2917  rgen2  2958  rgen2a  2960  nrex  2983  rexlimi  3006  rexlimiv  3009  sbcth2  3489  r19.2zb  4013  ral0  4028  unimax  4409  mpteq1  4665  mpteq2ia  4668  reusv2lem4  4798  wfisg  5632  fnopab  5931  fmpti  6291  sorpssuni  6844  sorpssint  6845  onssmin  6889  tfis  6946  omssnlim  6971  finds  6984  finds2  6986  opabex3  7038  wfr3  7322  seqomlem2  7433  findcard3  8088  fifo  8221  fisupcl  8258  dfom3  8427  cantnfvalf  8445  rankf  8540  scottex  8631  cplem1  8635  harcard  8687  cardiun  8691  r0weon  8718  acnnum  8758  alephon  8775  alephsmo  8808  alephf1ALT  8809  alephfplem4  8813  dfac5lem4  8832  dfacacn  8846  kmlem1  8855  cflem  8951  cflecard  8958  cfsmolem  8975  fin23lem17  9043  hsmexlem4  9134  omina  9392  0tsk  9456  inar1  9476  wfgru  9517  reclem2pr  9749  nnssre  10901  dfnn2  10910  dfnn3  10911  nnind  10915  nnsub  10936  dfuzi  11344  uzsupss  11656  cnref1o  11703  xrsupsslem  12009  xrinfmsslem  12010  xrsup0  12025  reltre  12041  rpltrp  12042  reltxrnmnf  12043  ser0f  12716  bccl  12971  hashkf  12981  hashbc  13094  wrdind  13328  sqrlem5  13835  rexuz3  13936  sqrtf  13951  ackbijnn  14399  incexclem  14407  prodf1f  14463  eff2  14668  reeff1  14689  sqrt2irr  14817  prmind2  15236  3prm  15244  phisum  15333  pockthi  15449  infpn2  15455  prminf  15457  prmreclem2  15459  prmrec  15464  1arith  15469  1arith2  15470  vdwlem13  15535  ramz  15567  prmgap  15601  prmgaplcm  15602  prmgapprmo  15604  prmlem1a  15651  xpsff1o  16051  isacs1i  16141  dmaf  16522  cdaf  16523  coapm  16544  lublecllem  16811  pmtrdifel  17723  pmtrdifwrdel  17728  odf  17779  efgrelexlemb  17986  dprd2da  18264  mgpf  18382  prdscrngd  18436  cnfld1  19590  cnsubglem  19614  cnmsubglem  19628  nn0srg  19635  rge0srg  19636  pmatcoe1fsupp  20325  isbasis3g  20564  basdif0  20568  distop  20610  mretopd  20706  2ndcsep  21072  refref  21126  kqf  21360  fbssfi  21451  filcon  21497  prdstmdd  21737  ustfilxp  21826  prdsxmslem2  22144  qdensere  22383  recld2  22425  isclmi0  22706  iscvsi  22737  ovolf  23057  dyadmax  23172  dveflem  23546  mdegxrf  23632  fta1  23867  vieta1  23871  aalioulem2  23892  taylfval  23917  pilem2  24010  pilem3  24011  recosf1o  24085  divlogrlim  24181  logcn  24193  ressatans  24461  leibpi  24469  ftalem3  24601  chtub  24737  2sqlem6  24948  2sqlem10  24953  chtppilim  24964  pntpbnd1  25075  pntlem3  25098  padicabvf  25120  axcontlem2  25645  isgrpoi  26736  isvciOLD  26819  cnidOLD  26821  isnvi  26852  ipasslem8  27076  hilid  27402  hlimf  27478  shsspwh  27487  pjrni  27945  pjmf1  27959  df0op2  27995  dfiop2  27996  hoaddcomi  28015  hoaddassi  28019  hocadddiri  28022  hocsubdiri  28023  hoaddid1i  28029  ho0coi  28031  hoid1i  28032  hoid1ri  28033  honegsubi  28039  hoddii  28232  lnopunilem2  28254  elunop2  28256  lnophm  28262  imaelshi  28301  cnlnadjlem8  28317  pjnmopi  28391  pjsdii  28398  pjddii  28399  pjtoi  28422  chirred  28638  nnindf  28952  nn0min  28954  esum2d  29482  dmvlsiga  29519  volmeas  29621  ddemeas  29626  sxbrsigalem3  29661  coinfliprv  29871  ballotlem7  29924  signsw0glem  29956  bnj580  30237  bnj1384  30354  bnj1497  30382  kur14lem9  30450  msrf  30693  dfon2lem7  30938  frinsg  30986  bdayfo  31074  nodense  31088  fobigcup  31177  nn0prpwlem  31487  topmeet  31529  onsucsuccmpi  31612  taupilemrplb  32343  relowlssretop  32387  ptrecube  32579  poimirlem27  32606  heicant  32614  mblfinlem1  32616  volsupnfl  32624  dvtan  32630  itg2addnc  32634  indexa  32698  sstotbnd2  32743  heiborlem7  32786  atpsubN  34057  idldil  34418  cdleme50ldil  34854  mzpclall  36308  dgraaf  36736  arearect  36820  areaquad  36821  clsk1indlem2  37360  clsk1indlem4  37362  prmunb2  37532  radcnvrat  37535  ssrab2f  38331  unirnmapsn  38401  ssmapsn  38403  upbdrech  38460  fsumiunss  38642  resincncf  38760  dmvolss  38878  volioof  38880  stoweidlem57  38950  wallispilem3  38960  stirlinglem13  38979  dirkertrigeqlem3  38993  fourierdlem62  39061  salexct  39228  salexct3  39236  salgencntex  39237  salgensscntex  39238  gsumge0cl  39264  0ome  39419  icoresmbl  39433  hoidmv1le  39484  smflimlem1  39657  smfpimbor1lem2  39684  fmtno4prm  40025  31prm  40050  tgoldbach  40232  tgoldbachOLD  40239  nbgrnself  40583  2zlidl  41724  2zrngagrp  41733  2zrngnmlid  41739  crhmsubc  41870  drhmsubc  41872  drngcat  41873  fldcat  41874  fldhmsubc  41876  crhmsubcALTV  41889  drhmsubcALTV  41891  drngcatALTV  41892  fldcatALTV  41893  fldhmsubcALTV  41895  zlmodzxznm  42080  ldepsnlinc  42091  nn0sumshdiglem2  42214  onsetrec  42250