Theorem rgen 3069

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3067

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

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

This theorem is referenced by:  ralel  3070  rgenw  3071  mprg  3073  mprgbir  3074  nrex  3080  rexlimivOLD  3191  rgen2  3205  r19.21be  3258  rexlimi  3265  rgen2a  3379  sbcth2  3906  r19.2zb  4519  unimax  4968  mpteq1OLD  5260  mpteq2iaOLD  5270  reusv2lem4  5419  wfisgOLD  6386  fnopab  6718  fmpti  7146  sorpssuni  7767  sorpssint  7768  onssmin  7828  tfis  7892  omssnlim  7918  finds  7936  finds2  7938  opabex3  8008  wfr3OLD  8394  seqomlem2  8507  findcard3  9346  findcard3OLD  9347  fifo  9501  fisupcl  9538  dfom3  9716  cantnfvalf  9734  frinsg  9820  rankf  9863  scottex  9954  cplem1  9958  harcard  10047  cardiun  10051  r0weon  10081  acnnum  10121  alephon  10138  alephsmo  10171  alephf1ALT  10172  alephfplem4  10176  dfac5lem4  10195  dfac5lem4OLD  10197  dfacacn  10211  kmlem1  10220  cflem  10314  cflemOLD  10315  cflecard  10322  cfsmolem  10339  fin23lem17  10407  hsmexlem4  10498  omina  10760  0tsk  10824  inar1  10844  wfgru  10885  reclem2pr  11117  nnssre  12297  nnsscn  12298  dfnn2  12306  dfnn3  12307  nnind  12311  nnsub  12337  dfuzi  12734  uzsupss  13005  cnref1o  13050  xrsupsslem  13369  xrinfmsslem  13370  xrsup0  13385  reltre  13402  rpltrp  13403  reltxrnmnf  13404  seqexw  14068  ser0f  14106  bccl  14371  hashkf  14381  hashbc  14502  wrdind  14770  01sqrexlem5  15295  sqrtf  15412  ackbijnn  15876  incexclem  15884  prodf1f  15940  eff2  16147  reeff1  16168  sqrt2irr  16297  prmind2  16732  3prm  16741  phisum  16837  pockthi  16954  infpn2  16960  prminf  16962  prmreclem2  16964  prmrec  16969  1arith  16974  1arith2  16975  vdwlem13  17040  ramz  17072  prmgap  17106  prmgaplcm  17107  prmgapprmo  17109  prmlem1a  17154  xpsff1o  17627  isacs1i  17715  dmaf  18116  cdaf  18117  coapm  18138  lublecllem  18430  smndex1mnd  18945  pwmnd  18972  pmtrdifel  19522  pmtrdifwrdel  19527  odf  19579  efgrelexlemb  19792  dprd2da  20086  rngmgpf  20184  mgpf  20275  prdscrngd  20345  crhmsubc  20704  drhmsubc  20804  drngcat  20805  fldcat  20806  fldhmsubc  20808  cnfld1  21429  cnfld1OLD  21430  cnsubglem  21456  cnmsubglem  21471  nn0srg  21478  rge0srg  21479  pzriprnglem4  21518  pzriprnglem9  21523  pzriprnglem14  21528  pmatcoe1fsupp  22728  isbasis3g  22977  basdif0  22981  distop  23023  mretopd  23121  2ndcsep  23488  refref  23542  kqf  23776  fbssfi  23866  filconn  23912  prdstmdd  24153  ustfilxp  24242  prdsxmslem2  24563  qdensere  24811  recld2  24855  isclmi0  25150  iscvsi  25181  ovolf  25536  dyadmax  25652  dveflem  26037  mdegxrf  26127  fta1  26368  vieta1  26372  aalioulem2  26393  taylfval  26418  pilem2  26514  pilem3  26515  recosf1o  26595  divlogrlim  26695  logcn  26707  ressatans  26995  leibpi  27003  ftalem3  27136  chtub  27274  2sqlem6  27485  2sqlem10  27490  2sqreulem4  27516  chtppilim  27537  pntpbnd1  27648  pntlem3  27671  padicabvf  27693  bdayfo  27740  nodense  27755  oldf  27914  scutfo  27960  addsfo  28034  negsf  28102  negsfo  28103  subsfo  28113  dfn0s2  28354  n0subs  28378  dfnns2  28380  zs12bday  28442  axcontlem2  28998  nbgrnself  29394  vtxdginducedm1  29579  isgrpoi  30530  isvciOLD  30612  cnidOLD  30614  isnvi  30645  ipasslem8  30869  hilid  31193  hlimf  31269  shsspwh  31278  pjrni  31734  pjmf1  31748  df0op2  31784  dfiop2  31785  hoaddcomi  31804  hoaddassi  31808  hocadddiri  31811  hocsubdiri  31812  hoaddridi  31818  ho0coi  31820  hoid1i  31821  hoid1ri  31822  honegsubi  31828  hoddii  32021  lnopunilem2  32043  elunop2  32045  lnophm  32051  imaelshi  32090  cnlnadjlem8  32106  pjnmopi  32180  pjsdii  32187  pjddii  32188  pjtoi  32211  chirred  32427  nnindf  32823  nn0min  32824  wrdt2ind  32920  zringfrac  33547  ccfldsrarelvec  33681  constrconj  33735  2sqr3minply  33738  esum2d  34057  dmvlsiga  34093  volmeas  34195  ddemeas  34200  sxbrsigalem3  34237  coinfliprv  34447  ballotlem7  34500  signsw0glem  34530  rpsqrtcn  34570  tgoldbachgt  34640  bnj580  34889  bnj1384  35008  bnj1497  35036  kur14lem9  35182  sat1el2xp  35347  msrf  35510  dfon2lem7  35753  fobigcup  35864  nn0prpwlem  36288  topmeet  36330  onsucsuccmpi  36409  taupilemrplb  37286  relowlssretop  37329  ptrecube  37580  poimirlem27  37607  heicant  37615  mblfinlem1  37617  volsupnfl  37625  dvtan  37630  itg2addnc  37634  indexa  37693  sstotbnd2  37734  heiborlem7  37777  atpsubN  39710  idldil  40071  cdleme50ldil  40505  mzpclall  42683  dgraaf  43104  arearect  43176  areaquad  43177  onintunirab  43188  onsupuni  43190  infordmin  43494  omiscard  43505  clsk1indlem2  44004  clsk1indlem4  44006  mnuunid  44246  mnurndlem1  44250  prmunb2  44280  radcnvrat  44283  trwf  44909  unirnmapsn  45121  ssmapsn  45123  upbdrech  45220  supminfxr  45379  supminfxr2  45384  supminfxrrnmpt  45386  rexanuz2nf  45408  fsumiunss  45496  resincncf  45796  dmvolss  45906  volioof  45908  stoweidlem57  45978  wallispilem3  45988  stirlinglem13  46007  dirkertrigeqlem3  46021  fourierdlem62  46089  salexct  46255  salexct3  46263  salgencntex  46264  salgensscntex  46265  gsumge0cl  46292  0ome  46450  icoresmbl  46464  hoidmv1le  46515  smflimlem1  46692  smfpimbor1lem2  46720  smfliminflem  46751  natlocalincr  46795  ralndv1  47020  fmtno4prm  47449  31prm  47471  tgoldbach  47691  nn0mnd  47902  2zlidl  47963  2zrngagrp  47972  2zrngnmlid  47978  crhmsubcALTV  48050  drhmsubcALTV  48052  drngcatALTV  48053  fldcatALTV  48054  fldhmsubcALTV  48056  zlmodzxznm  48226  ldepsnlinc  48237  nn0sumshdiglem2  48356  itcovalpclem1  48404  itcovalt2lem1  48409  rrx2xpref1o  48452  setc2othin  48723  onsetrec  48800