Theorem rgen 3073

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3063

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

This theorem depends on definitions:  df-bi 206  df-ral 3068

This theorem is referenced by:  ralel  3074  rgenw  3075  mprg  3077  mprgbir  3078  rgen2  3126  r19.21be  3133  rgen2a  3155  nrex  3196  rexlimiv  3208  rexlimi  3243  sbcth2  3813  r19.2zb  4423  ral0OLD  4444  unimax  4874  mpteq1OLD  5164  mpteq2iaOLD  5174  reusv2lem4  5319  wfisgOLD  6242  fnopab  6555  fmpti  6968  sorpssuni  7563  sorpssint  7564  onssmin  7619  tfis  7676  omssnlim  7702  finds  7719  finds2  7721  opabex3  7783  wfr3OLD  8140  seqomlem2  8252  findcard3  8987  fifo  9121  fisupcl  9158  dfom3  9335  cantnfvalf  9353  frinsg  9440  rankf  9483  scottex  9574  cplem1  9578  harcard  9667  cardiun  9671  r0weon  9699  acnnum  9739  alephon  9756  alephsmo  9789  alephf1ALT  9790  alephfplem4  9794  dfac5lem4  9813  dfacacn  9828  kmlem1  9837  cflem  9933  cflecard  9940  cfsmolem  9957  fin23lem17  10025  hsmexlem4  10116  omina  10378  0tsk  10442  inar1  10462  wfgru  10503  reclem2pr  10735  nnssre  11907  nnsscn  11908  dfnn2  11916  dfnn3  11917  nnind  11921  nnsub  11947  dfuzi  12341  uzsupss  12609  cnref1o  12654  xrsupsslem  12970  xrinfmsslem  12971  xrsup0  12986  reltre  13003  rpltrp  13004  reltxrnmnf  13005  seqexw  13665  ser0f  13704  bccl  13964  hashkf  13974  hashbc  14093  wrdind  14363  sqrlem5  14886  sqrtf  15003  ackbijnn  15468  incexclem  15476  prodf1f  15532  eff2  15736  reeff1  15757  sqrt2irr  15886  prmind2  16318  3prm  16327  phisum  16419  pockthi  16536  infpn2  16542  prminf  16544  prmreclem2  16546  prmrec  16551  1arith  16556  1arith2  16557  vdwlem13  16622  ramz  16654  prmgap  16688  prmgaplcm  16689  prmgapprmo  16691  prmlem1a  16736  xpsff1o  17195  isacs1i  17283  dmaf  17680  cdaf  17681  coapm  17702  lublecllem  17993  smndex1mnd  18464  pwmnd  18491  pmtrdifel  19003  pmtrdifwrdel  19008  odf  19060  efgrelexlemb  19271  dprd2da  19560  mgpf  19713  prdscrngd  19767  cnfld1  20535  cnsubglem  20559  cnmsubglem  20573  nn0srg  20580  rge0srg  20581  pmatcoe1fsupp  21758  isbasis3g  22007  basdif0  22011  distop  22053  mretopd  22151  2ndcsep  22518  refref  22572  kqf  22806  fbssfi  22896  filconn  22942  prdstmdd  23183  ustfilxp  23272  prdsxmslem2  23591  qdensere  23839  recld2  23883  isclmi0  24167  iscvsi  24198  ovolf  24551  dyadmax  24667  dveflem  25048  mdegxrf  25138  fta1  25373  vieta1  25377  aalioulem2  25398  taylfval  25423  pilem2  25516  pilem3  25517  recosf1o  25596  divlogrlim  25695  logcn  25707  ressatans  25989  leibpi  25997  ftalem3  26129  chtub  26265  2sqlem6  26476  2sqlem10  26481  2sqreulem4  26507  chtppilim  26528  pntpbnd1  26639  pntlem3  26662  padicabvf  26684  axcontlem2  27236  nbgrnself  27629  vtxdginducedm1  27813  isgrpoi  28761  isvciOLD  28843  cnidOLD  28845  isnvi  28876  ipasslem8  29100  hilid  29424  hlimf  29500  shsspwh  29509  pjrni  29965  pjmf1  29979  df0op2  30015  dfiop2  30016  hoaddcomi  30035  hoaddassi  30039  hocadddiri  30042  hocsubdiri  30043  hoaddid1i  30049  ho0coi  30051  hoid1i  30052  hoid1ri  30053  honegsubi  30059  hoddii  30252  lnopunilem2  30274  elunop2  30276  lnophm  30282  imaelshi  30321  cnlnadjlem8  30337  pjnmopi  30411  pjsdii  30418  pjddii  30419  pjtoi  30442  chirred  30658  nnindf  31035  nn0min  31036  wrdt2ind  31127  ccfldsrarelvec  31643  esum2d  31961  dmvlsiga  31997  volmeas  32099  ddemeas  32104  sxbrsigalem3  32139  coinfliprv  32349  ballotlem7  32402  signsw0glem  32432  rpsqrtcn  32473  tgoldbachgt  32543  bnj580  32793  bnj1384  32912  bnj1497  32940  kur14lem9  33076  sat1el2xp  33241  msrf  33404  dfon2lem7  33671  bdayfo  33807  nodense  33822  oldf  33968  scutfo  34011  fobigcup  34129  nn0prpwlem  34438  topmeet  34480  onsucsuccmpi  34559  taupilemrplb  35418  relowlssretop  35461  ptrecube  35704  poimirlem27  35731  heicant  35739  mblfinlem1  35741  volsupnfl  35749  dvtan  35754  itg2addnc  35758  indexa  35818  sstotbnd2  35859  heiborlem7  35902  atpsubN  37694  idldil  38055  cdleme50ldil  38489  mzpclall  40465  dgraaf  40888  arearect  40962  areaquad  40963  infordmin  41037  clsk1indlem2  41541  clsk1indlem4  41543  mnuunid  41784  mnurndlem1  41788  prmunb2  41818  radcnvrat  41821  unirnmapsn  42643  ssmapsn  42645  upbdrech  42734  supminfxr  42894  supminfxr2  42899  supminfxrrnmpt  42901  fsumiunss  43006  resincncf  43306  dmvolss  43416  volioof  43418  stoweidlem57  43488  wallispilem3  43498  stirlinglem13  43517  dirkertrigeqlem3  43531  fourierdlem62  43599  salexct  43763  salexct3  43771  salgencntex  43772  salgensscntex  43773  gsumge0cl  43799  0ome  43957  icoresmbl  43971  hoidmv1le  44022  smflimlem1  44193  smfpimbor1lem2  44220  smfliminflem  44250  ralndv1  44484  fmtno4prm  44915  31prm  44937  tgoldbach  45157  nn0mnd  45261  2zlidl  45380  2zrngagrp  45389  2zrngnmlid  45395  crhmsubc  45524  drhmsubc  45526  drngcat  45527  fldcat  45528  fldhmsubc  45530  crhmsubcALTV  45542  drhmsubcALTV  45544  drngcatALTV  45545  fldcatALTV  45546  fldhmsubcALTV  45548  zlmodzxznm  45726  ldepsnlinc  45737  nn0sumshdiglem2  45856  itcovalpclem1  45904  itcovalt2lem1  45909  rrx2xpref1o  45952  setc2othin  46225  onsetrec  46299