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  3334  sbcth2  3823  unimax  4888  reusv2lem4  5338  fnopab  6630  fmpti  7058  sorpssuni  7679  sorpssint  7680  onssmin  7739  tfis  7799  omssnlim  7825  finds  7840  finds2  7842  opabex3  7913  seqomlem2  8383  findcard3  9186  fifo  9338  fisupcl  9376  dfom3  9559  cantnfvalf  9577  frinsg  9666  rankf  9709  scottex  9800  cplem1  9804  harcard  9893  cardiun  9897  r0weon  9925  acnnum  9965  alephon  9982  alephsmo  10015  alephf1ALT  10016  alephfplem4  10020  dfac5lem4  10039  dfac5lem4OLD  10041  dfacacn  10055  kmlem1  10064  cflem  10158  cflemOLD  10159  cflecard  10166  cfsmolem  10183  fin23lem17  10251  hsmexlem4  10342  omina  10605  0tsk  10669  inar1  10689  wfgru  10730  reclem2pr  10962  nnssre  12169  nnsscn  12170  dfnn2  12178  dfnn3  12179  nnind  12183  nnsub  12212  dfuzi  12611  uzsupss  12881  cnref1o  12926  xrsupsslem  13250  xrinfmsslem  13251  xrsup0  13266  reltre  13284  rpltrp  13285  reltxrnmnf  13286  seqexw  13970  ser0f  14008  bccl  14275  hashkf  14285  hashbc  14406  wrdind  14675  01sqrexlem5  15199  sqrtf  15317  ackbijnn  15784  incexclem  15792  prodf1f  15848  eff2  16057  reeff1  16078  sqrt2irr  16207  prmind2  16645  3prm  16654  phisum  16752  pockthi  16869  infpn2  16875  prminf  16877  prmreclem2  16879  prmrec  16884  1arith  16889  1arith2  16890  vdwlem13  16955  ramz  16987  prmgap  17021  prmgaplcm  17022  prmgapprmo  17024  prmlem1a  17068  xpsff1o  17522  isacs1i  17614  dmaf  18007  cdaf  18008  coapm  18029  lublecllem  18315  chninf  18592  ex-chn1  18594  ex-chn2  18595  smndex1mnd  18872  pwmnd  18899  pmtrdifel  19446  pmtrdifwrdel  19451  odf  19503  efgrelexlemb  19716  dprd2da  20010  rngmgpf  20129  mgpf  20220  prdscrngd  20292  crhmsubc  20650  drhmsubc  20749  drngcat  20750  fldcat  20751  fldhmsubc  20753  cnfld1  21383  cnfld1OLD  21384  cnsubglem  21405  cnmsubglem  21420  nn0srg  21427  rge0srg  21428  pzriprnglem4  21474  pzriprnglem9  21479  pzriprnglem14  21484  pmatcoe1fsupp  22676  isbasis3g  22924  basdif0  22928  distop  22970  mretopd  23067  2ndcsep  23434  refref  23488  kqf  23722  fbssfi  23812  filconn  23858  prdstmdd  24099  ustfilxp  24188  prdsxmslem2  24504  qdensere  24744  recld2  24790  isclmi0  25075  iscvsi  25106  ovolf  25459  dyadmax  25575  dveflem  25956  mdegxrf  26043  fta1  26285  vieta1  26289  aalioulem2  26310  taylfval  26335  pilem2  26430  pilem3  26431  recosf1o  26512  divlogrlim  26612  logcn  26624  ressatans  26911  leibpi  26919  ftalem3  27052  chtub  27189  2sqlem6  27400  2sqlem10  27405  2sqreulem4  27431  chtppilim  27452  pntpbnd1  27563  pntlem3  27586  padicabvf  27608  bdayfo  27655  nodense  27670  oldf  27843  cutsfo  27911  addsfo  27989  negsf  28058  negsfo  28059  subsfo  28071  oniso  28277  dfn0s2  28338  n0subs  28369  bdayn0sf1o  28376  dfnns2  28378  zsoring  28415  bdaypw2n0bndlem  28469  bdayfinbndlem2  28474  z12zsodd  28488  axcontlem2  29048  nbgrnself  29442  vtxdginducedm1  29627  isgrpoi  30584  isvciOLD  30666  cnidOLD  30668  isnvi  30699  ipasslem8  30923  hilid  31247  hlimf  31323  shsspwh  31332  pjrni  31788  pjmf1  31802  df0op2  31838  dfiop2  31839  hoaddcomi  31858  hoaddassi  31862  hocadddiri  31865  hocsubdiri  31866  hoaddridi  31872  ho0coi  31874  hoid1i  31875  hoid1ri  31876  honegsubi  31882  hoddii  32075  lnopunilem2  32097  elunop2  32099  lnophm  32105  imaelshi  32144  cnlnadjlem8  32160  pjnmopi  32234  pjsdii  32241  pjddii  32242  pjtoi  32265  chirred  32481  nnindf  32908  nn0min  32909  wrdt2ind  33028  zringfrac  33629  ccfldsrarelvec  33831  constrconj  33905  2sqr3minply  33940  cos9thpiminply  33948  esum2d  34253  dmvlsiga  34289  volmeas  34391  ddemeas  34396  sxbrsigalem3  34432  coinfliprv  34643  ballotlem7  34696  signsw0glem  34713  rpsqrtcn  34753  tgoldbachgt  34823  bnj580  35071  bnj1384  35190  bnj1497  35218  fineqvnttrclse  35284  onvf1odlem1  35301  kur14lem9  35412  sat1el2xp  35577  msrf  35740  dfon2lem7  35985  fobigcup  36096  nn0prpwlem  36520  topmeet  36562  onsucsuccmpi  36641  dfttc4lem2  36727  taupilemrplb  37650  relowlssretop  37693  ptrecube  37955  poimirlem27  37982  heicant  37990  mblfinlem1  37992  volsupnfl  38000  dvtan  38005  itg2addnc  38009  indexa  38068  sstotbnd2  38109  heiborlem7  38152  disjimeceqim  39139  atpsubN  40213  idldil  40574  cdleme50ldil  41008  mzpclall  43173  dgraaf  43593  arearect  43661  areaquad  43662  onintunirab  43673  onsupuni  43675  infordmin  43977  omiscard  43988  clsk1indlem2  44487  clsk1indlem4  44489  mnuunid  44722  mnurndlem1  44726  prmunb2  44756  radcnvrat  44759  trwf  45404  rankrelp  45405  wfac8prim  45447  unirnmapsn  45661  ssmapsn  45663  upbdrech  45756  supminfxr  45910  supminfxr2  45915  supminfxrrnmpt  45917  rexanuz2nf  45938  fsumiunss  46023  resincncf  46321  dmvolss  46431  volioof  46433  stoweidlem57  46503  wallispilem3  46513  stirlinglem13  46532  dirkertrigeqlem3  46546  fourierdlem62  46614  salexct  46780  salexct3  46788  salgencntex  46789  salgensscntex  46790  gsumge0cl  46817  0ome  46975  icoresmbl  46989  hoidmv1le  47040  smflimlem1  47217  smfpimbor1lem2  47245  smfliminflem  47276  natlocalincr  47322  sinnpoly  47351  ralndv1  47565  fmtno4prm  48050  31prm  48072  tgoldbach  48305  gpg5grlim  48581  gpg5grlic  48582  nn0mnd  48667  2zlidl  48728  2zrngagrp  48737  2zrngnmlid  48743  crhmsubcALTV  48815  drhmsubcALTV  48817  drngcatALTV  48818  fldcatALTV  48819  fldhmsubcALTV  48821  zlmodzxznm  48985  ldepsnlinc  48996  nn0sumshdiglem2  49110  itcovalpclem1  49158  itcovalt2lem1  49163  rrx2xpref1o  49206  slotresfo  49386  basresposfo  49465  oppff1  49635  setc2othin  49953  setcsnterm  49977  onsetrec  50195