Theorem rgen 3050

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

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

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 3049

This theorem is referenced by:  ralel  3051  rgenw  3052  mprg  3054  mprgbir  3055  nrex  3061  rgen2  3173  r19.21be  3226  rexlimi  3233  rgen2a  3338  sbcth2  3831  r19.2zb  4445  unimax  4895  reusv2lem4  5341  fnopab  6624  fmpti  7051  sorpssuni  7671  sorpssint  7672  onssmin  7731  tfis  7791  omssnlim  7817  finds  7832  finds2  7834  opabex3  7905  seqomlem2  8376  findcard3  9174  fifo  9323  fisupcl  9361  dfom3  9544  cantnfvalf  9562  frinsg  9651  rankf  9694  scottex  9785  cplem1  9789  harcard  9878  cardiun  9882  r0weon  9910  acnnum  9950  alephon  9967  alephsmo  10000  alephf1ALT  10001  alephfplem4  10005  dfac5lem4  10024  dfac5lem4OLD  10026  dfacacn  10040  kmlem1  10049  cflem  10143  cflemOLD  10144  cflecard  10151  cfsmolem  10168  fin23lem17  10236  hsmexlem4  10327  omina  10589  0tsk  10653  inar1  10673  wfgru  10714  reclem2pr  10946  nnssre  12136  nnsscn  12137  dfnn2  12145  dfnn3  12146  nnind  12150  nnsub  12176  dfuzi  12570  uzsupss  12840  cnref1o  12885  xrsupsslem  13208  xrinfmsslem  13209  xrsup0  13224  reltre  13242  rpltrp  13243  reltxrnmnf  13244  seqexw  13926  ser0f  13964  bccl  14231  hashkf  14241  hashbc  14362  wrdind  14631  01sqrexlem5  15155  sqrtf  15273  ackbijnn  15737  incexclem  15745  prodf1f  15801  eff2  16010  reeff1  16031  sqrt2irr  16160  prmind2  16598  3prm  16607  phisum  16704  pockthi  16821  infpn2  16827  prminf  16829  prmreclem2  16831  prmrec  16836  1arith  16841  1arith2  16842  vdwlem13  16907  ramz  16939  prmgap  16973  prmgaplcm  16974  prmgapprmo  16976  prmlem1a  17020  xpsff1o  17473  isacs1i  17565  dmaf  17958  cdaf  17959  coapm  17980  lublecllem  18266  chninf  18543  ex-chn1  18545  ex-chn2  18546  smndex1mnd  18820  pwmnd  18847  pmtrdifel  19394  pmtrdifwrdel  19399  odf  19451  efgrelexlemb  19664  dprd2da  19958  rngmgpf  20077  mgpf  20168  prdscrngd  20242  crhmsubc  20599  drhmsubc  20698  drngcat  20699  fldcat  20700  fldhmsubc  20702  cnfld1  21332  cnfld1OLD  21333  cnsubglem  21354  cnmsubglem  21369  nn0srg  21376  rge0srg  21377  pzriprnglem4  21423  pzriprnglem9  21428  pzriprnglem14  21433  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  28945  nbgrnself  29339  vtxdginducedm1  29524  isgrpoi  30480  isvciOLD  30562  cnidOLD  30564  isnvi  30595  ipasslem8  30819  hilid  31143  hlimf  31219  shsspwh  31228  pjrni  31684  pjmf1  31698  df0op2  31734  dfiop2  31735  hoaddcomi  31754  hoaddassi  31758  hocadddiri  31761  hocsubdiri  31762  hoaddridi  31768  ho0coi  31770  hoid1i  31771  hoid1ri  31772  honegsubi  31778  hoddii  31971  lnopunilem2  31993  elunop2  31995  lnophm  32001  imaelshi  32040  cnlnadjlem8  32056  pjnmopi  32130  pjsdii  32137  pjddii  32138  pjtoi  32161  chirred  32377  nnindf  32807  nn0min  32808  wrdt2ind  32941  zringfrac  33526  ccfldsrarelvec  33705  constrconj  33779  2sqr3minply  33814  cos9thpiminply  33822  esum2d  34127  dmvlsiga  34163  volmeas  34265  ddemeas  34270  sxbrsigalem3  34306  coinfliprv  34517  ballotlem7  34570  signsw0glem  34587  rpsqrtcn  34627  tgoldbachgt  34697  bnj580  34946  bnj1384  35065  bnj1497  35093  fineqvnttrclse  35165  onvf1odlem1  35168  kur14lem9  35279  sat1el2xp  35444  msrf  35607  dfon2lem7  35852  fobigcup  35963  nn0prpwlem  36387  topmeet  36429  onsucsuccmpi  36508  taupilemrplb  37385  relowlssretop  37428  ptrecube  37681  poimirlem27  37708  heicant  37716  mblfinlem1  37718  volsupnfl  37726  dvtan  37731  itg2addnc  37735  indexa  37794  sstotbnd2  37835  heiborlem7  37878  atpsubN  39873  idldil  40234  cdleme50ldil  40668  mzpclall  42845  dgraaf  43265  arearect  43333  areaquad  43334  onintunirab  43345  onsupuni  43347  infordmin  43650  omiscard  43661  clsk1indlem2  44160  clsk1indlem4  44162  mnuunid  44395  mnurndlem1  44399  prmunb2  44429  radcnvrat  44432  trwf  45077  rankrelp  45078  wfac8prim  45120  unirnmapsn  45336  ssmapsn  45338  upbdrech  45431  supminfxr  45587  supminfxr2  45592  supminfxrrnmpt  45594  rexanuz2nf  45615  fsumiunss  45700  resincncf  45998  dmvolss  46108  volioof  46110  stoweidlem57  46180  wallispilem3  46190  stirlinglem13  46209  dirkertrigeqlem3  46223  fourierdlem62  46291  salexct  46457  salexct3  46465  salgencntex  46466  salgensscntex  46467  gsumge0cl  46494  0ome  46652  icoresmbl  46666  hoidmv1le  46717  smflimlem1  46894  smfpimbor1lem2  46922  smfliminflem  46953  natlocalincr  46999  sinnpoly  47016  ralndv1  47230  fmtno4prm  47700  31prm  47722  tgoldbach  47942  gpg5grlim  48218  gpg5grlic  48219  nn0mnd  48304  2zlidl  48365  2zrngagrp  48374  2zrngnmlid  48380  crhmsubcALTV  48452  drhmsubcALTV  48454  drngcatALTV  48455  fldcatALTV  48456  fldhmsubcALTV  48458  zlmodzxznm  48623  ldepsnlinc  48634  nn0sumshdiglem2  48748  itcovalpclem1  48796  itcovalt2lem1  48801  rrx2xpref1o  48844  slotresfo  49024  basresposfo  49103  oppff1  49274  setc2othin  49592  setcsnterm  49616  onsetrec  49834