Theorem rgen 3082

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∀wral 3080

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

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

This theorem is used by:  ralel  3083  rgenw  3084  mprg  3086  mprgbir  3087  nrex  3094  rgen2  3206  r19.21be  3259  rexlimi  3266  rgen2a  3360  sbcth2  3835  unimax  4908  reusv2lem4  5367  fnopab  6699  fmpti  7136  sorpssuni  7772  sorpssint  7773  onssmin  7830  tfis  7890  omssnlim  7916  finds  7932  finds2  7934  opabex3  8003  seqomlem2  8489  findcard3  9302  fifo  9451  fisupcl  9489  dfom3  9675  cantnfvalf  9693  frinsg  9782  rankf  9829  scottex  9960  scottexOLD  9961  cplem1  9977  cplem1OLD  9978  harcard  10086  cardiun  10090  r0weon  10118  acnnum  10158  alephon  10175  alephsmo  10208  alephf1ALT  10209  alephfplem4  10213  dfac5lem4  10232  dfacacn  10247  kmlem1  10256  cflem  10350  cflecard  10357  cfsmolem  10375  fin23lem17  10443  hsmexlem4  10534  omina  10803  0tsk  10867  inar1  10887  wfgru  10928  reclem2pr  11160  nnssre  12366  nnsscn  12367  dfnn2  12375  dfnn3  12376  nnind  12380  nnsub  12409  dfuzi  12817  uzsupss  13094  cnref1o  13140  xrsupsslem  13464  xrinfmsslem  13465  xrsup0  13480  reltre  13498  rpltrp  13499  reltxrnmnf  13500  seqexw  14187  ser0f  14225  bccl  14493  hashkf  14503  hashbc  14625  wrdind  14899  sgnrn  15280  01sqrexlem5  15442  sqrtf  15560  ackbijnn  16026  incexclem  16034  prodf1f  16090  eff2  16296  reeff1  16317  sqrt2irr  16446  prmind2  16889  3prm  16898  phisum  16997  pockthi  17114  infpn2  17120  prminf  17122  prmreclem2  17124  prmrec  17129  1arith  17134  1arith2  17135  vdwlem13  17200  ramz  17232  prmgap  17266  prmgaplcm  17267  prmgapprmo  17269  prmlem1a  17313  xpsff1o  17768  isacs1i  17860  dmaf  18253  cdaf  18254  coapm  18275  lublecllem  18561  chninf  18838  ex-chn1  18840  ex-chn2  18841  smndex1mnd  19138  pwmnd  19172  pmtrdifel  19724  pmtrdifwrdel  19729  odf  19781  efgrelexlemb  19994  dprd2da  20288  rngmgpf  20409  mgpf  20505  prdscrngd  20581  crhmsubc  20964  drhmsubc  21068  drngcat  21069  fldcat  21070  fldhmsubc  21072  cnfld1  21733  cnsubglem  21752  cnmsubglem  21766  nn0srg  21773  rge0srg  21774  pzriprnglem4  21820  pzriprnglem9  21825  pzriprnglem14  21830  pmatcoe1fsupp  23049  isbasis3g  23297  basdif0  23301  distop  23343  mretopd  23440  2ndcsep  23808  refref  23862  kqf  24096  fbssfi  24186  filconn  24232  prdstmdd  24473  ustfilxp  24562  prdsxmslem2  24878  qdensere  25118  recld2  25164  isclmi0  25449  iscvsi  25480  ovolf  25833  dyadmax  25949  dveflem  26329  mdegxrf  26416  fta1  26659  vieta1  26665  aalioulem2  26690  taylfval  26716  pilem2  26809  pilem3  26810  recosf1o  26893  divlogrlim  26993  logcn  27005  ressatans  27292  leibpi  27300  ftalem3  27432  chtub  27569  2sqlem6  27780  2sqlem10  27785  2sqreulem4  27811  chtppilim  27832  pntpbnd1  27943  pntlem3  27966  padicabvf  27988  bdayfo  28064  nodense  28079  oldf  28253  cutsfo  28321  addsfo  28399  negsf  28468  negsfo  28469  subsfo  28481  oniso  28687  dfn0s2  28748  n0subs  28779  bdayn0sf1o  28786  dfnns2  28788  zsoring  28825  bdaypw2n0bndlem  28879  bdayfinbndlem2  28884  z12zsodd  28898  axcontlem2  29573  nbgrnself  29970  vtxdginducedm1  30154  isgrpoi  31130  isvciOLD  31212  cnidOLD  31214  isnvi  31245  ipasslem8  31469  hilid  31793  hlimf  31869  shsspwh  31878  pjrni  32334  pjmf1  32348  df0op2  32384  dfiop2  32385  hoaddcomi  32404  hoaddassi  32408  hocadddiri  32411  hocsubdiri  32412  hoaddridi  32418  ho0coi  32420  hoid1i  32421  hoid1ri  32422  honegsubi  32428  hoddii  32621  lnopunilem2  32643  elunop2  32645  lnophm  32651  imaelshi  32690  cnlnadjlem8  32706  pjnmopi  32780  pjsdii  32787  pjddii  32788  pjtoi  32811  chirred  33027  nnindf  33481  nn0min  33482  wrdt2ind  33586  zringfrac  34156  ccfldsrarelvec  34373  constrconj  34447  2sqr3minply  34482  cos9thpiminply  34490  esum2d  34795  dmvlsiga  34831  volmeas  34934  ddemeas  34939  sxbrsigalem3  34974  coinfliprv  35185  ballotlem7  35238  signsw0glem  35252  rpsqrtcn  35292  tgoldbachgt  35362  bnj580  35613  bnj1384  35732  bnj1497  35760  soinfdom  35800  rankfo  35817  fineqvnttrclse  35892  jf1  36010  onvf1odlem1  36031  kur14lem9  36146  sat1el2xp  36311  msrf  36474  dfon2lem7  36729  fobigcup  36840  nn0prpwlem  37288  topmeet  37330  onsucsuccmpi  37409  dfttc4lem2  37495  taupilemrplb  38433  relowlssretop  38478  ptrecube  38730  poimirlem27  38757  heicant  38765  mblfinlem1  38767  volsupnfl  38775  dvtan  38780  itg2addnc  38784  indexa  38859  sstotbnd2  38900  heiborlem7  38943  disjimeceqim  39928  atpsubN  41002  idldil  41363  cdleme50ldil  41797  mzpclall  43931  dgraaf  44341  arearect  44409  areaquad  44410  onintunirab  44421  onsupuni  44423  infordmin  44725  omiscard  44736  clsk1indlem2  45234  clsk1indlem4  45236  mnuunid  45453  mnurndlem1  45457  prmunb2  45487  radcnvrat  45490  trwf  46144  rankrelp  46145  wfac8prim  46187  hfstructwe  46234  unirnmapsn  46432  ssmapsn  46434  upbdrech  46526  supminfxr  46679  supminfxr2  46684  supminfxrrnmpt  46686  rexanuz2nf  46707  fsumiunss  46792  resincncf  47090  dmvolss  47200  volioof  47202  stoweidlem57  47272  wallispilem3  47282  stirlinglem13  47301  dirkertrigeqlem3  47315  fourierdlem62  47383  salexct  47549  salexct3  47557  salgencntex  47558  salgensscntex  47559  gsumge0cl  47586  0ome  47744  icoresmbl  47758  hoidmv1le  47809  smflimlem1  47986  smfpimbor1lem2  48014  smfliminflem  48045  ralndv1  48381  fmtno4prm  48865  31prm  48887  tgoldbach  49120  gpg5grlim  49396  gpg5grlic  49397  nn0mnd  49481  2zlidl  49542  2zrngagrp  49551  2zrngnmlid  49557  crhmsubcALTV  49629  drhmsubcALTV  49631  drngcatALTV  49632  fldcatALTV  49633  fldhmsubcALTV  49635  zlmodzxznm  49814  ldepsnlinc  49825  nn0sumshdiglem2  49939  itcovalpclem1  49987  itcovalt2lem1  49992  slotresfo  50218  basresposfo  50297  oppff1  50469  setc2othin  50806  setcsnterm  50830  parswapprop  50982  onsetrec  51081