Theorem rgen 3053

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3051

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 3052

This theorem is referenced by:  ralel  3054  rgenw  3055  mprg  3057  mprgbir  3058  nrex  3064  rgen2  3176  r19.21be  3229  rexlimi  3236  rgen2a  3341  sbcth2  3834  unimax  4900  reusv2lem4  5346  fnopab  6630  fmpti  7057  sorpssuni  7677  sorpssint  7678  onssmin  7737  tfis  7797  omssnlim  7823  finds  7838  finds2  7840  opabex3  7911  seqomlem2  8382  findcard3  9183  fifo  9335  fisupcl  9373  dfom3  9556  cantnfvalf  9574  frinsg  9663  rankf  9706  scottex  9797  cplem1  9801  harcard  9890  cardiun  9894  r0weon  9922  acnnum  9962  alephon  9979  alephsmo  10012  alephf1ALT  10013  alephfplem4  10017  dfac5lem4  10036  dfac5lem4OLD  10038  dfacacn  10052  kmlem1  10061  cflem  10155  cflemOLD  10156  cflecard  10163  cfsmolem  10180  fin23lem17  10248  hsmexlem4  10339  omina  10602  0tsk  10666  inar1  10686  wfgru  10727  reclem2pr  10959  nnssre  12149  nnsscn  12150  dfnn2  12158  dfnn3  12159  nnind  12163  nnsub  12189  dfuzi  12583  uzsupss  12853  cnref1o  12898  xrsupsslem  13222  xrinfmsslem  13223  xrsup0  13238  reltre  13256  rpltrp  13257  reltxrnmnf  13258  seqexw  13940  ser0f  13978  bccl  14245  hashkf  14255  hashbc  14376  wrdind  14645  01sqrexlem5  15169  sqrtf  15287  ackbijnn  15751  incexclem  15759  prodf1f  15815  eff2  16024  reeff1  16045  sqrt2irr  16174  prmind2  16612  3prm  16621  phisum  16718  pockthi  16835  infpn2  16841  prminf  16843  prmreclem2  16845  prmrec  16850  1arith  16855  1arith2  16856  vdwlem13  16921  ramz  16953  prmgap  16987  prmgaplcm  16988  prmgapprmo  16990  prmlem1a  17034  xpsff1o  17488  isacs1i  17580  dmaf  17973  cdaf  17974  coapm  17995  lublecllem  18281  chninf  18558  ex-chn1  18560  ex-chn2  18561  smndex1mnd  18835  pwmnd  18862  pmtrdifel  19409  pmtrdifwrdel  19414  odf  19466  efgrelexlemb  19679  dprd2da  19973  rngmgpf  20092  mgpf  20183  prdscrngd  20257  crhmsubc  20615  drhmsubc  20714  drngcat  20715  fldcat  20716  fldhmsubc  20718  cnfld1  21348  cnfld1OLD  21349  cnsubglem  21370  cnmsubglem  21385  nn0srg  21392  rge0srg  21393  pzriprnglem4  21439  pzriprnglem9  21444  pzriprnglem14  21449  pmatcoe1fsupp  22645  isbasis3g  22893  basdif0  22897  distop  22939  mretopd  23036  2ndcsep  23403  refref  23457  kqf  23691  fbssfi  23781  filconn  23827  prdstmdd  24068  ustfilxp  24157  prdsxmslem2  24473  qdensere  24713  recld2  24759  isclmi0  25054  iscvsi  25085  ovolf  25439  dyadmax  25555  dveflem  25939  mdegxrf  26029  fta1  26272  vieta1  26276  aalioulem2  26297  taylfval  26322  pilem2  26418  pilem3  26419  recosf1o  26500  divlogrlim  26600  logcn  26612  ressatans  26900  leibpi  26908  ftalem3  27041  chtub  27179  2sqlem6  27390  2sqlem10  27395  2sqreulem4  27421  chtppilim  27442  pntpbnd1  27553  pntlem3  27576  padicabvf  27598  bdayfo  27645  nodense  27660  oldf  27833  cutsfo  27901  addsfo  27979  negsf  28048  negsfo  28049  subsfo  28061  oniso  28267  dfn0s2  28328  n0subs  28359  bdayn0sf1o  28366  dfnns2  28368  zsoring  28405  bdaypw2n0bndlem  28459  bdayfinbndlem2  28464  z12zsodd  28478  axcontlem2  29038  nbgrnself  29432  vtxdginducedm1  29617  isgrpoi  30573  isvciOLD  30655  cnidOLD  30657  isnvi  30688  ipasslem8  30912  hilid  31236  hlimf  31312  shsspwh  31321  pjrni  31777  pjmf1  31791  df0op2  31827  dfiop2  31828  hoaddcomi  31847  hoaddassi  31851  hocadddiri  31854  hocsubdiri  31855  hoaddridi  31861  ho0coi  31863  hoid1i  31864  hoid1ri  31865  honegsubi  31871  hoddii  32064  lnopunilem2  32086  elunop2  32088  lnophm  32094  imaelshi  32133  cnlnadjlem8  32149  pjnmopi  32223  pjsdii  32230  pjddii  32231  pjtoi  32254  chirred  32470  nnindf  32900  nn0min  32901  wrdt2ind  33035  zringfrac  33635  ccfldsrarelvec  33828  constrconj  33902  2sqr3minply  33937  cos9thpiminply  33945  esum2d  34250  dmvlsiga  34286  volmeas  34388  ddemeas  34393  sxbrsigalem3  34429  coinfliprv  34640  ballotlem7  34693  signsw0glem  34710  rpsqrtcn  34750  tgoldbachgt  34820  bnj580  35069  bnj1384  35188  bnj1497  35216  fineqvnttrclse  35280  onvf1odlem1  35297  kur14lem9  35408  sat1el2xp  35573  msrf  35736  dfon2lem7  35981  fobigcup  36092  nn0prpwlem  36516  topmeet  36558  onsucsuccmpi  36637  taupilemrplb  37521  relowlssretop  37564  ptrecube  37817  poimirlem27  37844  heicant  37852  mblfinlem1  37854  volsupnfl  37862  dvtan  37867  itg2addnc  37871  indexa  37930  sstotbnd2  37971  heiborlem7  38014  atpsubN  40009  idldil  40370  cdleme50ldil  40804  mzpclall  42965  dgraaf  43385  arearect  43453  areaquad  43454  onintunirab  43465  onsupuni  43467  infordmin  43769  omiscard  43780  clsk1indlem2  44279  clsk1indlem4  44281  mnuunid  44514  mnurndlem1  44518  prmunb2  44548  radcnvrat  44551  trwf  45196  rankrelp  45197  wfac8prim  45239  unirnmapsn  45454  ssmapsn  45456  upbdrech  45549  supminfxr  45704  supminfxr2  45709  supminfxrrnmpt  45711  rexanuz2nf  45732  fsumiunss  45817  resincncf  46115  dmvolss  46225  volioof  46227  stoweidlem57  46297  wallispilem3  46307  stirlinglem13  46326  dirkertrigeqlem3  46340  fourierdlem62  46408  salexct  46574  salexct3  46582  salgencntex  46583  salgensscntex  46584  gsumge0cl  46611  0ome  46769  icoresmbl  46783  hoidmv1le  46834  smflimlem1  47011  smfpimbor1lem2  47039  smfliminflem  47070  natlocalincr  47116  sinnpoly  47133  ralndv1  47347  fmtno4prm  47817  31prm  47839  tgoldbach  48059  gpg5grlim  48335  gpg5grlic  48336  nn0mnd  48421  2zlidl  48482  2zrngagrp  48491  2zrngnmlid  48497  crhmsubcALTV  48569  drhmsubcALTV  48571  drngcatALTV  48572  fldcatALTV  48573  fldhmsubcALTV  48575  zlmodzxznm  48739  ldepsnlinc  48750  nn0sumshdiglem2  48864  itcovalpclem1  48912  itcovalt2lem1  48917  rrx2xpref1o  48960  slotresfo  49140  basresposfo  49219  oppff1  49389  setc2othin  49707  setcsnterm  49731  onsetrec  49949