Theorem rgen 3078

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  ralel  3079  rgenw  3080  mprg  3082  mprgbir  3083  nrex  3090  rgen2  3202  r19.21be  3255  rexlimi  3262  rgen2a  3356  sbcth2  3830  unimax  4904  reusv2lem4  5362  fnopab  6677  fmpti  7112  sorpssuni  7748  sorpssint  7749  onssmin  7806  tfis  7866  omssnlim  7892  finds  7908  finds2  7910  opabex3  7979  seqomlem2  8464  findcard3  9277  fifo  9427  fisupcl  9465  dfom3  9651  cantnfvalf  9669  frinsg  9758  rankf  9805  scottex  9936  scottexOLD  9937  cplem1  9953  cplem1OLD  9954  harcard  10062  cardiun  10066  r0weon  10094  acnnum  10134  alephon  10151  alephsmo  10184  alephf1ALT  10185  alephfplem4  10189  dfac5lem4  10208  dfacacn  10223  kmlem1  10232  cflem  10326  cflecard  10333  cfsmolem  10351  fin23lem17  10419  hsmexlem4  10510  omina  10779  0tsk  10843  inar1  10863  wfgru  10904  reclem2pr  11136  nnssre  12342  nnsscn  12343  dfnn2  12351  dfnn3  12352  nnind  12356  nnsub  12385  dfuzi  12793  uzsupss  13070  cnref1o  13116  xrsupsslem  13440  xrinfmsslem  13441  xrsup0  13456  reltre  13474  rpltrp  13475  reltxrnmnf  13476  seqexw  14163  ser0f  14201  bccl  14469  hashkf  14479  hashbc  14601  wrdind  14875  sgnrn  15256  01sqrexlem5  15418  sqrtf  15536  ackbijnn  16002  incexclem  16010  prodf1f  16066  eff2  16272  reeff1  16293  sqrt2irr  16422  prmind2  16865  3prm  16874  phisum  16973  pockthi  17090  infpn2  17096  prminf  17098  prmreclem2  17100  prmrec  17105  1arith  17110  1arith2  17111  vdwlem13  17176  ramz  17208  prmgap  17242  prmgaplcm  17243  prmgapprmo  17245  prmlem1a  17289  xpsff1o  17744  isacs1i  17836  dmaf  18229  cdaf  18230  coapm  18251  lublecllem  18537  chninf  18814  ex-chn1  18816  ex-chn2  18817  smndex1mnd  19114  pwmnd  19148  pmtrdifel  19699  pmtrdifwrdel  19704  odf  19756  efgrelexlemb  19969  dprd2da  20263  rngmgpf  20384  mgpf  20480  prdscrngd  20556  crhmsubc  20939  drhmsubc  21043  drngcat  21044  fldcat  21045  fldhmsubc  21047  cnfld1  21708  cnsubglem  21727  cnmsubglem  21741  nn0srg  21748  rge0srg  21749  pzriprnglem4  21795  pzriprnglem9  21800  pzriprnglem14  21805  pmatcoe1fsupp  23024  isbasis3g  23272  basdif0  23276  distop  23318  mretopd  23415  2ndcsep  23783  refref  23837  kqf  24071  fbssfi  24161  filconn  24207  prdstmdd  24448  ustfilxp  24537  prdsxmslem2  24853  qdensere  25093  recld2  25139  isclmi0  25424  iscvsi  25455  ovolf  25808  dyadmax  25924  dveflem  26304  mdegxrf  26391  fta1  26634  vieta1  26640  aalioulem2  26665  taylfval  26691  pilem2  26784  pilem3  26785  recosf1o  26868  divlogrlim  26968  logcn  26980  ressatans  27267  leibpi  27275  ftalem3  27407  chtub  27544  2sqlem6  27755  2sqlem10  27760  2sqreulem4  27786  chtppilim  27807  pntpbnd1  27918  pntlem3  27941  padicabvf  27963  bdayfo  28039  nodense  28054  oldf  28228  cutsfo  28296  addsfo  28374  negsf  28443  negsfo  28444  subsfo  28456  oniso  28662  dfn0s2  28723  n0subs  28754  bdayn0sf1o  28761  dfnns2  28763  zsoring  28800  bdaypw2n0bndlem  28854  bdayfinbndlem2  28859  z12zsodd  28873  axcontlem2  29548  nbgrnself  29945  vtxdginducedm1  30129  isgrpoi  31105  isvciOLD  31187  cnidOLD  31189  isnvi  31220  ipasslem8  31444  hilid  31768  hlimf  31844  shsspwh  31853  pjrni  32309  pjmf1  32323  df0op2  32359  dfiop2  32360  hoaddcomi  32379  hoaddassi  32383  hocadddiri  32386  hocsubdiri  32387  hoaddridi  32393  ho0coi  32395  hoid1i  32396  hoid1ri  32397  honegsubi  32403  hoddii  32596  lnopunilem2  32618  elunop2  32620  lnophm  32626  imaelshi  32665  cnlnadjlem8  32681  pjnmopi  32755  pjsdii  32762  pjddii  32763  pjtoi  32786  chirred  33002  nnindf  33457  nn0min  33458  wrdt2ind  33562  zringfrac  34132  ccfldsrarelvec  34349  constrconj  34423  2sqr3minply  34458  cos9thpiminply  34466  esum2d  34771  dmvlsiga  34807  volmeas  34910  ddemeas  34915  sxbrsigalem3  34950  coinfliprv  35161  ballotlem7  35214  signsw0glem  35228  rpsqrtcn  35268  tgoldbachgt  35338  bnj580  35589  bnj1384  35708  bnj1497  35736  soinfdom  35768  rankfo  35787  fineqvnttrclse  35848  onvf1odlem1  35950  kur14lem9  36065  sat1el2xp  36230  msrf  36393  dfon2lem7  36643  fobigcup  36754  nn0prpwlem  37202  topmeet  37244  onsucsuccmpi  37323  dfttc4lem2  37409  taupilemrplb  38334  relowlssretop  38379  ptrecube  38631  poimirlem27  38658  heicant  38666  mblfinlem1  38668  volsupnfl  38676  dvtan  38681  itg2addnc  38685  indexa  38760  sstotbnd2  38801  heiborlem7  38844  disjimeceqim  39829  atpsubN  40903  idldil  41264  cdleme50ldil  41698  mzpclall  43831  dgraaf  44242  arearect  44310  areaquad  44311  onintunirab  44322  onsupuni  44324  infordmin  44626  omiscard  44637  clsk1indlem2  45135  clsk1indlem4  45137  mnuunid  45354  mnurndlem1  45358  prmunb2  45388  radcnvrat  45391  trwf  46042  rankrelp  46043  wfac8prim  46085  unirnmapsn  46320  ssmapsn  46322  upbdrech  46414  supminfxr  46567  supminfxr2  46572  supminfxrrnmpt  46574  rexanuz2nf  46595  fsumiunss  46680  resincncf  46978  dmvolss  47088  volioof  47090  stoweidlem57  47160  wallispilem3  47170  stirlinglem13  47189  dirkertrigeqlem3  47203  fourierdlem62  47271  salexct  47437  salexct3  47445  salgencntex  47446  salgensscntex  47447  gsumge0cl  47474  0ome  47632  icoresmbl  47646  hoidmv1le  47697  smflimlem1  47874  smfpimbor1lem2  47902  smfliminflem  47933  ralndv1  48268  fmtno4prm  48753  31prm  48775  tgoldbach  49008  gpg5grlim  49284  gpg5grlic  49285  nn0mnd  49369  2zlidl  49430  2zrngagrp  49439  2zrngnmlid  49445  crhmsubcALTV  49517  drhmsubcALTV  49519  drngcatALTV  49520  fldcatALTV  49521  fldhmsubcALTV  49523  zlmodzxznm  49702  ldepsnlinc  49713  nn0sumshdiglem2  49827  itcovalpclem1  49875  itcovalt2lem1  49880  slotresfo  50106  basresposfo  50185  oppff1  50357  setc2othin  50694  setcsnterm  50718  parswapprop  50870  onsetrec  50969