Theorem rgen 3054

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

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

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

This theorem is referenced by:  ralel  3055  rgenw  3056  mprg  3058  mprgbir  3059  nrex  3066  rgen2  3178  r19.21be  3231  rexlimi  3238  rgen2a  3343  sbcth2  3836  unimax  4902  reusv2lem4  5348  fnopab  6638  fmpti  7066  sorpssuni  7687  sorpssint  7688  onssmin  7747  tfis  7807  omssnlim  7833  finds  7848  finds2  7850  opabex3  7921  seqomlem2  8392  findcard3  9195  fifo  9347  fisupcl  9385  dfom3  9568  cantnfvalf  9586  frinsg  9675  rankf  9718  scottex  9809  cplem1  9813  harcard  9902  cardiun  9906  r0weon  9934  acnnum  9974  alephon  9991  alephsmo  10024  alephf1ALT  10025  alephfplem4  10029  dfac5lem4  10048  dfac5lem4OLD  10050  dfacacn  10064  kmlem1  10073  cflem  10167  cflemOLD  10168  cflecard  10175  cfsmolem  10192  fin23lem17  10260  hsmexlem4  10351  omina  10614  0tsk  10678  inar1  10698  wfgru  10739  reclem2pr  10971  nnssre  12161  nnsscn  12162  dfnn2  12170  dfnn3  12171  nnind  12175  nnsub  12201  dfuzi  12595  uzsupss  12865  cnref1o  12910  xrsupsslem  13234  xrinfmsslem  13235  xrsup0  13250  reltre  13268  rpltrp  13269  reltxrnmnf  13270  seqexw  13952  ser0f  13990  bccl  14257  hashkf  14267  hashbc  14388  wrdind  14657  01sqrexlem5  15181  sqrtf  15299  ackbijnn  15763  incexclem  15771  prodf1f  15827  eff2  16036  reeff1  16057  sqrt2irr  16186  prmind2  16624  3prm  16633  phisum  16730  pockthi  16847  infpn2  16853  prminf  16855  prmreclem2  16857  prmrec  16862  1arith  16867  1arith2  16868  vdwlem13  16933  ramz  16965  prmgap  16999  prmgaplcm  17000  prmgapprmo  17002  prmlem1a  17046  xpsff1o  17500  isacs1i  17592  dmaf  17985  cdaf  17986  coapm  18007  lublecllem  18293  chninf  18570  ex-chn1  18572  ex-chn2  18573  smndex1mnd  18847  pwmnd  18874  pmtrdifel  19421  pmtrdifwrdel  19426  odf  19478  efgrelexlemb  19691  dprd2da  19985  rngmgpf  20104  mgpf  20195  prdscrngd  20269  crhmsubc  20627  drhmsubc  20726  drngcat  20727  fldcat  20728  fldhmsubc  20730  cnfld1  21360  cnfld1OLD  21361  cnsubglem  21382  cnmsubglem  21397  nn0srg  21404  rge0srg  21405  pzriprnglem4  21451  pzriprnglem9  21456  pzriprnglem14  21461  pmatcoe1fsupp  22657  isbasis3g  22905  basdif0  22909  distop  22951  mretopd  23048  2ndcsep  23415  refref  23469  kqf  23703  fbssfi  23793  filconn  23839  prdstmdd  24080  ustfilxp  24169  prdsxmslem2  24485  qdensere  24725  recld2  24771  isclmi0  25066  iscvsi  25097  ovolf  25451  dyadmax  25567  dveflem  25951  mdegxrf  26041  fta1  26284  vieta1  26288  aalioulem2  26309  taylfval  26334  pilem2  26430  pilem3  26431  recosf1o  26512  divlogrlim  26612  logcn  26624  ressatans  26912  leibpi  26920  ftalem3  27053  chtub  27191  2sqlem6  27402  2sqlem10  27407  2sqreulem4  27433  chtppilim  27454  pntpbnd1  27565  pntlem3  27588  padicabvf  27610  bdayfo  27657  nodense  27672  oldf  27845  cutsfo  27913  addsfo  27991  negsf  28060  negsfo  28061  subsfo  28073  oniso  28279  dfn0s2  28340  n0subs  28371  bdayn0sf1o  28378  dfnns2  28380  zsoring  28417  bdaypw2n0bndlem  28471  bdayfinbndlem2  28476  z12zsodd  28490  axcontlem2  29050  nbgrnself  29444  vtxdginducedm1  29629  isgrpoi  30585  isvciOLD  30667  cnidOLD  30669  isnvi  30700  ipasslem8  30924  hilid  31248  hlimf  31324  shsspwh  31333  pjrni  31789  pjmf1  31803  df0op2  31839  dfiop2  31840  hoaddcomi  31859  hoaddassi  31863  hocadddiri  31866  hocsubdiri  31867  hoaddridi  31873  ho0coi  31875  hoid1i  31876  hoid1ri  31877  honegsubi  31883  hoddii  32076  lnopunilem2  32098  elunop2  32100  lnophm  32106  imaelshi  32145  cnlnadjlem8  32161  pjnmopi  32235  pjsdii  32242  pjddii  32243  pjtoi  32266  chirred  32482  nnindf  32910  nn0min  32911  wrdt2ind  33045  zringfrac  33646  ccfldsrarelvec  33848  constrconj  33922  2sqr3minply  33957  cos9thpiminply  33965  esum2d  34270  dmvlsiga  34306  volmeas  34408  ddemeas  34413  sxbrsigalem3  34449  coinfliprv  34660  ballotlem7  34713  signsw0glem  34730  rpsqrtcn  34770  tgoldbachgt  34840  bnj580  35088  bnj1384  35207  bnj1497  35235  fineqvnttrclse  35299  onvf1odlem1  35316  kur14lem9  35427  sat1el2xp  35592  msrf  35755  dfon2lem7  36000  fobigcup  36111  nn0prpwlem  36535  topmeet  36577  onsucsuccmpi  36656  taupilemrplb  37572  relowlssretop  37615  ptrecube  37868  poimirlem27  37895  heicant  37903  mblfinlem1  37905  volsupnfl  37913  dvtan  37918  itg2addnc  37922  indexa  37981  sstotbnd2  38022  heiborlem7  38065  disjimeceqim  39052  atpsubN  40126  idldil  40487  cdleme50ldil  40921  mzpclall  43081  dgraaf  43501  arearect  43569  areaquad  43570  onintunirab  43581  onsupuni  43583  infordmin  43885  omiscard  43896  clsk1indlem2  44395  clsk1indlem4  44397  mnuunid  44630  mnurndlem1  44634  prmunb2  44664  radcnvrat  44667  trwf  45312  rankrelp  45313  wfac8prim  45355  unirnmapsn  45569  ssmapsn  45571  upbdrech  45664  supminfxr  45819  supminfxr2  45824  supminfxrrnmpt  45826  rexanuz2nf  45847  fsumiunss  45932  resincncf  46230  dmvolss  46340  volioof  46342  stoweidlem57  46412  wallispilem3  46422  stirlinglem13  46441  dirkertrigeqlem3  46455  fourierdlem62  46523  salexct  46689  salexct3  46697  salgencntex  46698  salgensscntex  46699  gsumge0cl  46726  0ome  46884  icoresmbl  46898  hoidmv1le  46949  smflimlem1  47126  smfpimbor1lem2  47154  smfliminflem  47185  natlocalincr  47231  sinnpoly  47248  ralndv1  47462  fmtno4prm  47932  31prm  47954  tgoldbach  48174  gpg5grlim  48450  gpg5grlic  48451  nn0mnd  48536  2zlidl  48597  2zrngagrp  48606  2zrngnmlid  48612  crhmsubcALTV  48684  drhmsubcALTV  48686  drngcatALTV  48687  fldcatALTV  48688  fldhmsubcALTV  48690  zlmodzxznm  48854  ldepsnlinc  48865  nn0sumshdiglem2  48979  itcovalpclem1  49027  itcovalt2lem1  49032  rrx2xpref1o  49075  slotresfo  49255  basresposfo  49334  oppff1  49504  setc2othin  49822  setcsnterm  49846  onsetrec  50064