Theorem rgen 3148

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3138

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

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

This theorem is referenced by:  ralel  3149  rgenw  3150  mprg  3152  mprgbir  3153  rgen2  3203  r19.21be  3210  rgen2a  3229  nrex  3269  rexlimiv  3280  rexlimi  3315  sbcth2  3866  r19.2zb  4440  ral0  4455  unimax  4873  mpteq1  5153  mpteq2ia  5156  reusv2lem4  5301  wfisg  6182  fnopab  6485  fmpti  6875  sorpssuni  7457  sorpssint  7458  onssmin  7511  tfis  7568  omssnlim  7593  finds  7607  finds2  7609  opabex3  7667  wfr3  7974  seqomlem2  8086  findcard3  8760  fifo  8895  fisupcl  8932  dfom3  9109  cantnfvalf  9127  rankf  9222  scottex  9313  cplem1  9317  harcard  9406  cardiun  9410  r0weon  9437  acnnum  9477  alephon  9494  alephsmo  9527  alephf1ALT  9528  alephfplem4  9532  dfac5lem4  9551  dfacacn  9566  kmlem1  9575  cflem  9667  cflecard  9674  cfsmolem  9691  fin23lem17  9759  hsmexlem4  9850  omina  10112  0tsk  10176  inar1  10196  wfgru  10237  reclem2pr  10469  nnssre  11641  nnsscn  11642  dfnn2  11650  dfnn3  11651  nnind  11655  nnsub  11680  dfuzi  12072  uzsupss  12339  cnref1o  12383  xrsupsslem  12699  xrinfmsslem  12700  xrsup0  12715  reltre  12732  rpltrp  12733  reltxrnmnf  12734  seqexw  13384  ser0f  13422  bccl  13681  hashkf  13691  hashbc  13810  wrdind  14083  sqrlem5  14605  sqrtf  14722  ackbijnn  15182  incexclem  15190  prodf1f  15247  eff2  15451  reeff1  15472  sqrt2irr  15601  prmind2  16028  3prm  16037  phisum  16126  pockthi  16242  infpn2  16248  prminf  16250  prmreclem2  16252  prmrec  16257  1arith  16262  1arith2  16263  vdwlem13  16328  ramz  16360  prmgap  16394  prmgaplcm  16395  prmgapprmo  16397  prmlem1a  16439  xpsff1o  16839  isacs1i  16927  dmaf  17308  cdaf  17309  coapm  17330  lublecllem  17597  smndex1mnd  18074  pwmnd  18101  pmtrdifel  18607  pmtrdifwrdel  18612  odf  18664  efgrelexlemb  18875  dprd2da  19163  mgpf  19308  prdscrngd  19362  cnfld1  20569  cnsubglem  20593  cnmsubglem  20607  nn0srg  20614  rge0srg  20615  pmatcoe1fsupp  21308  isbasis3g  21556  basdif0  21560  distop  21602  mretopd  21699  2ndcsep  22066  refref  22120  kqf  22354  fbssfi  22444  filconn  22490  prdstmdd  22731  ustfilxp  22820  prdsxmslem2  23138  qdensere  23377  recld2  23421  isclmi0  23701  iscvsi  23732  ovolf  24082  dyadmax  24198  dveflem  24575  mdegxrf  24661  fta1  24896  vieta1  24900  aalioulem2  24921  taylfval  24946  pilem2  25039  pilem3  25040  recosf1o  25118  divlogrlim  25217  logcn  25229  ressatans  25511  leibpi  25519  ftalem3  25651  chtub  25787  2sqlem6  25998  2sqlem10  26003  2sqreulem4  26029  chtppilim  26050  pntpbnd1  26161  pntlem3  26184  padicabvf  26206  axcontlem2  26750  nbgrnself  27140  vtxdginducedm1  27324  isgrpoi  28274  isvciOLD  28356  cnidOLD  28358  isnvi  28389  ipasslem8  28613  hilid  28937  hlimf  29013  shsspwh  29022  pjrni  29478  pjmf1  29492  df0op2  29528  dfiop2  29529  hoaddcomi  29548  hoaddassi  29552  hocadddiri  29555  hocsubdiri  29556  hoaddid1i  29562  ho0coi  29564  hoid1i  29565  hoid1ri  29566  honegsubi  29572  hoddii  29765  lnopunilem2  29787  elunop2  29789  lnophm  29795  imaelshi  29834  cnlnadjlem8  29850  pjnmopi  29924  pjsdii  29931  pjddii  29932  pjtoi  29955  chirred  30171  nnindf  30534  nn0min  30536  wrdt2ind  30627  ccfldsrarelvec  31056  esum2d  31352  dmvlsiga  31388  volmeas  31490  ddemeas  31495  sxbrsigalem3  31530  coinfliprv  31740  ballotlem7  31793  signsw0glem  31823  rpsqrtcn  31864  tgoldbachgt  31934  bnj580  32185  bnj1384  32304  bnj1497  32332  kur14lem9  32461  sat1el2xp  32626  msrf  32789  dfon2lem7  33034  frinsg  33087  bdayfo  33182  nodense  33196  fobigcup  33361  nn0prpwlem  33670  topmeet  33712  onsucsuccmpi  33791  taupilemrplb  34600  relowlssretop  34643  ptrecube  34891  poimirlem27  34918  heicant  34926  mblfinlem1  34928  volsupnfl  34936  dvtan  34941  itg2addnc  34945  indexa  35007  sstotbnd2  35051  heiborlem7  35094  atpsubN  36888  idldil  37249  cdleme50ldil  37683  mzpclall  39322  dgraaf  39745  arearect  39820  areaquad  39821  infordmin  39897  clsk1indlem2  40390  clsk1indlem4  40392  mnuunid  40611  mnurndlem1  40615  prmunb2  40641  radcnvrat  40644  unirnmapsn  41475  ssmapsn  41477  upbdrech  41570  supminfxr  41738  supminfxr2  41743  supminfxrrnmpt  41745  fsumiunss  41854  resincncf  42156  dmvolss  42269  volioof  42271  stoweidlem57  42341  wallispilem3  42351  stirlinglem13  42370  dirkertrigeqlem3  42384  fourierdlem62  42452  salexct  42616  salexct3  42624  salgencntex  42625  salgensscntex  42626  gsumge0cl  42652  0ome  42810  icoresmbl  42824  hoidmv1le  42875  smflimlem1  43046  smfpimbor1lem2  43073  smfliminflem  43103  ralndv1  43303  fmtno4prm  43736  31prm  43759  tgoldbach  43981  nn0mnd  44085  2zlidl  44204  2zrngagrp  44213  2zrngnmlid  44219  crhmsubc  44348  drhmsubc  44350  drngcat  44351  fldcat  44352  fldhmsubc  44354  crhmsubcALTV  44366  drhmsubcALTV  44368  drngcatALTV  44369  fldcatALTV  44370  fldhmsubcALTV  44372  zlmodzxznm  44551  ldepsnlinc  44562  nn0sumshdiglem2  44681  rrx2xpref1o  44704  onsetrec  44809