Theorem rgen 3046

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

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

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

This theorem is referenced by:  ralel  3047  rgenw  3048  mprg  3050  mprgbir  3051  nrex  3057  rexlimivOLD  3163  rgen2  3177  r19.21be  3230  rexlimi  3237  rgen2a  3345  sbcth2  3847  r19.2zb  4459  unimax  4908  reusv2lem4  5356  fnopab  6656  fmpti  7084  sorpssuni  7708  sorpssint  7709  onssmin  7768  tfis  7831  omssnlim  7857  finds  7872  finds2  7874  opabex3  7946  seqomlem2  8419  findcard3  9229  findcard3OLD  9230  fifo  9383  fisupcl  9421  dfom3  9600  cantnfvalf  9618  frinsg  9704  rankf  9747  scottex  9838  cplem1  9842  harcard  9931  cardiun  9935  r0weon  9965  acnnum  10005  alephon  10022  alephsmo  10055  alephf1ALT  10056  alephfplem4  10060  dfac5lem4  10079  dfac5lem4OLD  10081  dfacacn  10095  kmlem1  10104  cflem  10198  cflemOLD  10199  cflecard  10206  cfsmolem  10223  fin23lem17  10291  hsmexlem4  10382  omina  10644  0tsk  10708  inar1  10728  wfgru  10769  reclem2pr  11001  nnssre  12190  nnsscn  12191  dfnn2  12199  dfnn3  12200  nnind  12204  nnsub  12230  dfuzi  12625  uzsupss  12899  cnref1o  12944  xrsupsslem  13267  xrinfmsslem  13268  xrsup0  13283  reltre  13301  rpltrp  13302  reltxrnmnf  13303  seqexw  13982  ser0f  14020  bccl  14287  hashkf  14297  hashbc  14418  wrdind  14687  01sqrexlem5  15212  sqrtf  15330  ackbijnn  15794  incexclem  15802  prodf1f  15858  eff2  16067  reeff1  16088  sqrt2irr  16217  prmind2  16655  3prm  16664  phisum  16761  pockthi  16878  infpn2  16884  prminf  16886  prmreclem2  16888  prmrec  16893  1arith  16898  1arith2  16899  vdwlem13  16964  ramz  16996  prmgap  17030  prmgaplcm  17031  prmgapprmo  17033  prmlem1a  17077  xpsff1o  17530  isacs1i  17618  dmaf  18011  cdaf  18012  coapm  18033  lublecllem  18319  smndex1mnd  18837  pwmnd  18864  pmtrdifel  19410  pmtrdifwrdel  19415  odf  19467  efgrelexlemb  19680  dprd2da  19974  rngmgpf  20066  mgpf  20157  prdscrngd  20231  crhmsubc  20591  drhmsubc  20690  drngcat  20691  fldcat  20692  fldhmsubc  20694  cnfld1  21305  cnfld1OLD  21306  cnsubglem  21332  cnmsubglem  21347  nn0srg  21354  rge0srg  21355  pzriprnglem4  21394  pzriprnglem9  21399  pzriprnglem14  21404  pmatcoe1fsupp  22588  isbasis3g  22836  basdif0  22840  distop  22882  mretopd  22979  2ndcsep  23346  refref  23400  kqf  23634  fbssfi  23724  filconn  23770  prdstmdd  24011  ustfilxp  24100  prdsxmslem2  24417  qdensere  24657  recld2  24703  isclmi0  24998  iscvsi  25029  ovolf  25383  dyadmax  25499  dveflem  25883  mdegxrf  25973  fta1  26216  vieta1  26220  aalioulem2  26241  taylfval  26266  pilem2  26362  pilem3  26363  recosf1o  26444  divlogrlim  26544  logcn  26556  ressatans  26844  leibpi  26852  ftalem3  26985  chtub  27123  2sqlem6  27334  2sqlem10  27339  2sqreulem4  27365  chtppilim  27386  pntpbnd1  27497  pntlem3  27520  padicabvf  27542  bdayfo  27589  nodense  27604  oldf  27765  scutfo  27816  addsfo  27890  negsf  27958  negsfo  27959  subsfo  27969  onsiso  28169  dfn0s2  28224  n0subs  28253  bdayn0sf1o  28259  dfnns2  28261  zs12bday  28343  axcontlem2  28892  nbgrnself  29286  vtxdginducedm1  29471  isgrpoi  30427  isvciOLD  30509  cnidOLD  30511  isnvi  30542  ipasslem8  30766  hilid  31090  hlimf  31166  shsspwh  31175  pjrni  31631  pjmf1  31645  df0op2  31681  dfiop2  31682  hoaddcomi  31701  hoaddassi  31705  hocadddiri  31708  hocsubdiri  31709  hoaddridi  31715  ho0coi  31717  hoid1i  31718  hoid1ri  31719  honegsubi  31725  hoddii  31918  lnopunilem2  31940  elunop2  31942  lnophm  31948  imaelshi  31987  cnlnadjlem8  32003  pjnmopi  32077  pjsdii  32084  pjddii  32085  pjtoi  32108  chirred  32324  nnindf  32744  nn0min  32745  wrdt2ind  32875  zringfrac  33525  ccfldsrarelvec  33666  constrconj  33735  2sqr3minply  33770  cos9thpiminply  33778  esum2d  34083  dmvlsiga  34119  volmeas  34221  ddemeas  34226  sxbrsigalem3  34263  coinfliprv  34474  ballotlem7  34527  signsw0glem  34544  rpsqrtcn  34584  tgoldbachgt  34654  bnj580  34903  bnj1384  35022  bnj1497  35050  onvf1odlem1  35090  kur14lem9  35201  sat1el2xp  35366  msrf  35529  dfon2lem7  35777  fobigcup  35888  nn0prpwlem  36310  topmeet  36352  onsucsuccmpi  36431  taupilemrplb  37308  relowlssretop  37351  ptrecube  37614  poimirlem27  37641  heicant  37649  mblfinlem1  37651  volsupnfl  37659  dvtan  37664  itg2addnc  37668  indexa  37727  sstotbnd2  37768  heiborlem7  37811  atpsubN  39747  idldil  40108  cdleme50ldil  40542  mzpclall  42715  dgraaf  43136  arearect  43204  areaquad  43205  onintunirab  43216  onsupuni  43218  infordmin  43521  omiscard  43532  clsk1indlem2  44031  clsk1indlem4  44033  mnuunid  44266  mnurndlem1  44270  prmunb2  44300  radcnvrat  44303  trwf  44949  rankrelp  44950  wfac8prim  44992  unirnmapsn  45208  ssmapsn  45210  upbdrech  45303  supminfxr  45460  supminfxr2  45465  supminfxrrnmpt  45467  rexanuz2nf  45488  fsumiunss  45573  resincncf  45873  dmvolss  45983  volioof  45985  stoweidlem57  46055  wallispilem3  46065  stirlinglem13  46084  dirkertrigeqlem3  46098  fourierdlem62  46166  salexct  46332  salexct3  46340  salgencntex  46341  salgensscntex  46342  gsumge0cl  46369  0ome  46527  icoresmbl  46541  hoidmv1le  46592  smflimlem1  46769  smfpimbor1lem2  46797  smfliminflem  46828  natlocalincr  46874  sinnpoly  46892  ralndv1  47106  fmtno4prm  47576  31prm  47598  tgoldbach  47818  gpg5grlic  48084  nn0mnd  48167  2zlidl  48228  2zrngagrp  48237  2zrngnmlid  48243  crhmsubcALTV  48315  drhmsubcALTV  48317  drngcatALTV  48318  fldcatALTV  48319  fldhmsubcALTV  48321  zlmodzxznm  48486  ldepsnlinc  48497  nn0sumshdiglem2  48611  itcovalpclem1  48659  itcovalt2lem1  48664  rrx2xpref1o  48707  slotresfo  48887  basresposfo  48966  oppff1  49137  setc2othin  49455  setcsnterm  49479  onsetrec  49697