Theorem rgen 3049

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3047

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

This theorem depends on definitions:  df-bi 207  df-ral 3048

This theorem is referenced by:  ralel  3050  rgenw  3051  mprg  3053  mprgbir  3054  nrex  3060  rgen2  3172  r19.21be  3225  rexlimi  3232  rgen2a  3337  sbcth2  3835  r19.2zb  4446  unimax  4895  reusv2lem4  5339  fnopab  6619  fmpti  7045  sorpssuni  7665  sorpssint  7666  onssmin  7725  tfis  7785  omssnlim  7811  finds  7826  finds2  7828  opabex3  7899  seqomlem2  8370  findcard3  9167  fifo  9316  fisupcl  9354  dfom3  9537  cantnfvalf  9555  frinsg  9644  rankf  9687  scottex  9778  cplem1  9782  harcard  9871  cardiun  9875  r0weon  9903  acnnum  9943  alephon  9960  alephsmo  9993  alephf1ALT  9994  alephfplem4  9998  dfac5lem4  10017  dfac5lem4OLD  10019  dfacacn  10033  kmlem1  10042  cflem  10136  cflemOLD  10137  cflecard  10144  cfsmolem  10161  fin23lem17  10229  hsmexlem4  10320  omina  10582  0tsk  10646  inar1  10666  wfgru  10707  reclem2pr  10939  nnssre  12129  nnsscn  12130  dfnn2  12138  dfnn3  12139  nnind  12143  nnsub  12169  dfuzi  12564  uzsupss  12838  cnref1o  12883  xrsupsslem  13206  xrinfmsslem  13207  xrsup0  13222  reltre  13240  rpltrp  13241  reltxrnmnf  13242  seqexw  13924  ser0f  13962  bccl  14229  hashkf  14239  hashbc  14360  wrdind  14629  01sqrexlem5  15153  sqrtf  15271  ackbijnn  15735  incexclem  15743  prodf1f  15799  eff2  16008  reeff1  16029  sqrt2irr  16158  prmind2  16596  3prm  16605  phisum  16702  pockthi  16819  infpn2  16825  prminf  16827  prmreclem2  16829  prmrec  16834  1arith  16839  1arith2  16840  vdwlem13  16905  ramz  16937  prmgap  16971  prmgaplcm  16972  prmgapprmo  16974  prmlem1a  17018  xpsff1o  17471  isacs1i  17563  dmaf  17956  cdaf  17957  coapm  17978  lublecllem  18264  chninf  18541  ex-chn1  18543  ex-chn2  18544  smndex1mnd  18818  pwmnd  18845  pmtrdifel  19393  pmtrdifwrdel  19398  odf  19450  efgrelexlemb  19663  dprd2da  19957  rngmgpf  20076  mgpf  20167  prdscrngd  20241  crhmsubc  20598  drhmsubc  20697  drngcat  20698  fldcat  20699  fldhmsubc  20701  cnfld1  21331  cnfld1OLD  21332  cnsubglem  21353  cnmsubglem  21368  nn0srg  21375  rge0srg  21376  pzriprnglem4  21422  pzriprnglem9  21427  pzriprnglem14  21432  pmatcoe1fsupp  22617  isbasis3g  22865  basdif0  22869  distop  22911  mretopd  23008  2ndcsep  23375  refref  23429  kqf  23663  fbssfi  23753  filconn  23799  prdstmdd  24040  ustfilxp  24129  prdsxmslem2  24445  qdensere  24685  recld2  24731  isclmi0  25026  iscvsi  25057  ovolf  25411  dyadmax  25527  dveflem  25911  mdegxrf  26001  fta1  26244  vieta1  26248  aalioulem2  26269  taylfval  26294  pilem2  26390  pilem3  26391  recosf1o  26472  divlogrlim  26572  logcn  26584  ressatans  26872  leibpi  26880  ftalem3  27013  chtub  27151  2sqlem6  27362  2sqlem10  27367  2sqreulem4  27393  chtppilim  27414  pntpbnd1  27525  pntlem3  27548  padicabvf  27570  bdayfo  27617  nodense  27632  oldf  27799  scutfo  27851  addsfo  27927  negsf  27995  negsfo  27996  subsfo  28006  onsiso  28206  dfn0s2  28261  n0subs  28290  bdayn0sf1o  28296  dfnns2  28298  zsoring  28333  zs12zodd  28393  zs12bday  28395  axcontlem2  28944  nbgrnself  29338  vtxdginducedm1  29523  isgrpoi  30476  isvciOLD  30558  cnidOLD  30560  isnvi  30591  ipasslem8  30815  hilid  31139  hlimf  31215  shsspwh  31224  pjrni  31680  pjmf1  31694  df0op2  31730  dfiop2  31731  hoaddcomi  31750  hoaddassi  31754  hocadddiri  31757  hocsubdiri  31758  hoaddridi  31764  ho0coi  31766  hoid1i  31767  hoid1ri  31768  honegsubi  31774  hoddii  31967  lnopunilem2  31989  elunop2  31991  lnophm  31997  imaelshi  32036  cnlnadjlem8  32052  pjnmopi  32126  pjsdii  32133  pjddii  32134  pjtoi  32157  chirred  32373  nnindf  32800  nn0min  32801  wrdt2ind  32932  zringfrac  33517  ccfldsrarelvec  33682  constrconj  33756  2sqr3minply  33791  cos9thpiminply  33799  esum2d  34104  dmvlsiga  34140  volmeas  34242  ddemeas  34247  sxbrsigalem3  34283  coinfliprv  34494  ballotlem7  34547  signsw0glem  34564  rpsqrtcn  34604  tgoldbachgt  34674  bnj580  34923  bnj1384  35042  bnj1497  35070  fineqvnttrclse  35142  onvf1odlem1  35145  kur14lem9  35256  sat1el2xp  35421  msrf  35584  dfon2lem7  35829  fobigcup  35940  nn0prpwlem  36362  topmeet  36404  onsucsuccmpi  36483  taupilemrplb  37360  relowlssretop  37403  ptrecube  37666  poimirlem27  37693  heicant  37701  mblfinlem1  37703  volsupnfl  37711  dvtan  37716  itg2addnc  37720  indexa  37779  sstotbnd2  37820  heiborlem7  37863  atpsubN  39798  idldil  40159  cdleme50ldil  40593  mzpclall  42766  dgraaf  43186  arearect  43254  areaquad  43255  onintunirab  43266  onsupuni  43268  infordmin  43571  omiscard  43582  clsk1indlem2  44081  clsk1indlem4  44083  mnuunid  44316  mnurndlem1  44320  prmunb2  44350  radcnvrat  44353  trwf  44998  rankrelp  44999  wfac8prim  45041  unirnmapsn  45257  ssmapsn  45259  upbdrech  45352  supminfxr  45508  supminfxr2  45513  supminfxrrnmpt  45515  rexanuz2nf  45536  fsumiunss  45621  resincncf  45919  dmvolss  46029  volioof  46031  stoweidlem57  46101  wallispilem3  46111  stirlinglem13  46130  dirkertrigeqlem3  46144  fourierdlem62  46212  salexct  46378  salexct3  46386  salgencntex  46387  salgensscntex  46388  gsumge0cl  46415  0ome  46573  icoresmbl  46587  hoidmv1le  46638  smflimlem1  46815  smfpimbor1lem2  46843  smfliminflem  46874  natlocalincr  46920  sinnpoly  46928  ralndv1  47142  fmtno4prm  47612  31prm  47634  tgoldbach  47854  gpg5grlim  48130  gpg5grlic  48131  nn0mnd  48216  2zlidl  48277  2zrngagrp  48286  2zrngnmlid  48292  crhmsubcALTV  48364  drhmsubcALTV  48366  drngcatALTV  48367  fldcatALTV  48368  fldhmsubcALTV  48370  zlmodzxznm  48535  ldepsnlinc  48546  nn0sumshdiglem2  48660  itcovalpclem1  48708  itcovalt2lem1  48713  rrx2xpref1o  48756  slotresfo  48936  basresposfo  49015  oppff1  49186  setc2othin  49504  setcsnterm  49528  onsetrec  49746