Theorem rgen 3079

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3077

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 3078

This theorem is used by:  ralel  3080  rgenw  3081  mprg  3083  mprgbir  3084  nrex  3091  rgen2  3203  r19.21be  3256  rexlimi  3263  rgen2a  3357  sbcth2  3831  unimax  4905  reusv2lem4  5363  fnopab  6669  fmpti  7104  sorpssuni  7737  sorpssint  7738  onssmin  7795  tfis  7855  omssnlim  7881  finds  7897  finds2  7899  opabex3  7968  seqomlem2  8445  findcard3  9258  fifo  9408  fisupcl  9446  dfom3  9632  cantnfvalf  9650  frinsg  9739  rankf  9784  scottex  9914  scottexOLD  9915  cplem1  9931  cplem1OLD  9932  harcard  10040  cardiun  10044  r0weon  10072  acnnum  10112  alephon  10129  alephsmo  10162  alephf1ALT  10163  alephfplem4  10167  dfac5lem4  10186  dfacacn  10201  kmlem1  10210  cflem  10304  cflecard  10311  cfsmolem  10329  fin23lem17  10397  hsmexlem4  10488  omina  10757  0tsk  10821  inar1  10841  wfgru  10882  reclem2pr  11114  nnssre  12320  nnsscn  12321  dfnn2  12329  dfnn3  12330  nnind  12334  nnsub  12363  dfuzi  12771  uzsupss  13048  cnref1o  13094  xrsupsslem  13418  xrinfmsslem  13419  xrsup0  13434  reltre  13452  rpltrp  13453  reltxrnmnf  13454  seqexw  14140  ser0f  14178  bccl  14446  hashkf  14456  hashbc  14578  wrdind  14851  sgnrn  15231  01sqrexlem5  15393  sqrtf  15511  ackbijnn  15977  incexclem  15985  prodf1f  16041  eff2  16247  reeff1  16268  sqrt2irr  16397  prmind2  16840  3prm  16849  phisum  16948  pockthi  17065  infpn2  17071  prminf  17073  prmreclem2  17075  prmrec  17080  1arith  17085  1arith2  17086  vdwlem13  17151  ramz  17183  prmgap  17217  prmgaplcm  17218  prmgapprmo  17220  prmlem1a  17264  xpsff1o  17719  isacs1i  17811  dmaf  18204  cdaf  18205  coapm  18226  lublecllem  18512  chninf  18789  ex-chn1  18791  ex-chn2  18792  smndex1mnd  19089  pwmnd  19123  pmtrdifel  19674  pmtrdifwrdel  19679  odf  19731  efgrelexlemb  19944  dprd2da  20238  rngmgpf  20359  mgpf  20455  prdscrngd  20531  crhmsubc  20914  drhmsubc  21018  drngcat  21019  fldcat  21020  fldhmsubc  21022  cnfld1  21683  cnsubglem  21702  cnmsubglem  21716  nn0srg  21723  rge0srg  21724  pzriprnglem4  21770  pzriprnglem9  21775  pzriprnglem14  21780  pmatcoe1fsupp  22999  isbasis3g  23247  basdif0  23251  distop  23293  mretopd  23390  2ndcsep  23758  refref  23812  kqf  24046  fbssfi  24136  filconn  24182  prdstmdd  24423  ustfilxp  24512  prdsxmslem2  24828  qdensere  25068  recld2  25114  isclmi0  25399  iscvsi  25430  ovolf  25783  dyadmax  25899  dveflem  26279  mdegxrf  26366  fta1  26611  vieta1  26617  aalioulem2  26642  taylfval  26668  pilem2  26761  pilem3  26762  recosf1o  26845  divlogrlim  26945  logcn  26957  ressatans  27244  leibpi  27252  ftalem3  27384  chtub  27521  2sqlem6  27732  2sqlem10  27737  2sqreulem4  27763  chtppilim  27784  pntpbnd1  27895  pntlem3  27918  padicabvf  27940  bdayfo  28016  nodense  28031  oldf  28205  cutsfo  28273  addsfo  28351  negsf  28420  negsfo  28421  subsfo  28433  oniso  28639  dfn0s2  28700  n0subs  28731  bdayn0sf1o  28738  dfnns2  28740  zsoring  28777  bdaypw2n0bndlem  28831  bdayfinbndlem2  28836  z12zsodd  28850  axcontlem2  29525  nbgrnself  29922  vtxdginducedm1  30106  isgrpoi  31082  isvciOLD  31164  cnidOLD  31166  isnvi  31197  ipasslem8  31421  hilid  31745  hlimf  31821  shsspwh  31830  pjrni  32286  pjmf1  32300  df0op2  32336  dfiop2  32337  hoaddcomi  32356  hoaddassi  32360  hocadddiri  32363  hocsubdiri  32364  hoaddridi  32370  ho0coi  32372  hoid1i  32373  hoid1ri  32374  honegsubi  32380  hoddii  32573  lnopunilem2  32595  elunop2  32597  lnophm  32603  imaelshi  32642  cnlnadjlem8  32658  pjnmopi  32732  pjsdii  32739  pjddii  32740  pjtoi  32763  chirred  32979  nnindf  33393  nn0min  33394  wrdt2ind  33498  zringfrac  34068  ccfldsrarelvec  34285  constrconj  34359  2sqr3minply  34394  cos9thpiminply  34402  esum2d  34707  dmvlsiga  34743  volmeas  34846  ddemeas  34851  sxbrsigalem3  34887  coinfliprv  35098  ballotlem7  35151  signsw0glem  35165  rpsqrtcn  35205  tgoldbachgt  35275  bnj580  35526  bnj1384  35645  bnj1497  35673  rankfo  35714  fineqvnttrclse  35765  onvf1odlem1  35855  kur14lem9  35948  sat1el2xp  36113  msrf  36276  dfon2lem7  36521  fobigcup  36632  nn0prpwlem  37080  topmeet  37122  onsucsuccmpi  37201  dfttc4lem2  37287  taupilemrplb  38209  relowlssretop  38254  ptrecube  38506  poimirlem27  38533  heicant  38541  mblfinlem1  38543  volsupnfl  38551  dvtan  38556  itg2addnc  38560  indexa  38635  sstotbnd2  38676  heiborlem7  38719  disjimeceqim  39704  atpsubN  40778  idldil  41139  cdleme50ldil  41573  mzpclall  43691  dgraaf  44107  arearect  44175  areaquad  44176  onintunirab  44187  onsupuni  44189  infordmin  44491  omiscard  44502  clsk1indlem2  45001  clsk1indlem4  45003  mnuunid  45220  mnurndlem1  45224  prmunb2  45254  radcnvrat  45257  trwf  45901  rankrelp  45902  wfac8prim  45944  unirnmapsn  46170  ssmapsn  46172  upbdrech  46264  supminfxr  46418  supminfxr2  46423  supminfxrrnmpt  46425  rexanuz2nf  46446  fsumiunss  46531  resincncf  46829  dmvolss  46939  volioof  46941  stoweidlem57  47011  wallispilem3  47021  stirlinglem13  47040  dirkertrigeqlem3  47054  fourierdlem62  47122  salexct  47288  salexct3  47296  salgencntex  47297  salgensscntex  47298  gsumge0cl  47325  0ome  47483  icoresmbl  47497  hoidmv1le  47548  smflimlem1  47725  smfpimbor1lem2  47753  smfliminflem  47784  ralndv1  48119  fmtno4prm  48604  31prm  48626  tgoldbach  48859  gpg5grlim  49135  gpg5grlic  49136  nn0mnd  49220  2zlidl  49281  2zrngagrp  49290  2zrngnmlid  49296  crhmsubcALTV  49368  drhmsubcALTV  49370  drngcatALTV  49371  fldcatALTV  49372  fldhmsubcALTV  49374  zlmodzxznm  49553  ldepsnlinc  49564  nn0sumshdiglem2  49678  itcovalpclem1  49726  itcovalt2lem1  49731  rrx2xpref1o  49774  slotresfo  49951  basresposfo  50030  oppff1  50200  setc2othin  50518  setcsnterm  50542  onsetrec  50745