Theorem rgen 3064

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  ralel  3065  rgenw  3066  mprg  3068  mprgbir  3069  nrex  3075  rexlimivOLD  3185  rgen2  3198  r19.21be  3250  rexlimi  3257  rgen2a  3368  sbcth2  3879  r19.2zb  4496  ral0OLD  4517  unimax  4949  mpteq1OLD  5243  mpteq2iaOLD  5253  reusv2lem4  5400  wfisgOLD  6356  fnopab  6689  fmpti  7112  sorpssuni  7722  sorpssint  7723  onssmin  7780  tfis  7844  omssnlim  7870  finds  7889  finds2  7891  opabex3  7954  wfr3OLD  8338  seqomlem2  8451  findcard3  9285  findcard3OLD  9286  fifo  9427  fisupcl  9464  dfom3  9642  cantnfvalf  9660  frinsg  9746  rankf  9789  scottex  9880  cplem1  9884  harcard  9973  cardiun  9977  r0weon  10007  acnnum  10047  alephon  10064  alephsmo  10097  alephf1ALT  10098  alephfplem4  10102  dfac5lem4  10121  dfacacn  10136  kmlem1  10145  cflem  10241  cflecard  10248  cfsmolem  10265  fin23lem17  10333  hsmexlem4  10424  omina  10686  0tsk  10750  inar1  10770  wfgru  10811  reclem2pr  11043  nnssre  12216  nnsscn  12217  dfnn2  12225  dfnn3  12226  nnind  12230  nnsub  12256  dfuzi  12653  uzsupss  12924  cnref1o  12969  xrsupsslem  13286  xrinfmsslem  13287  xrsup0  13302  reltre  13319  rpltrp  13320  reltxrnmnf  13321  seqexw  13982  ser0f  14021  bccl  14282  hashkf  14292  hashbc  14412  wrdind  14672  01sqrexlem5  15193  sqrtf  15310  ackbijnn  15774  incexclem  15782  prodf1f  15838  eff2  16042  reeff1  16063  sqrt2irr  16192  prmind2  16622  3prm  16631  phisum  16723  pockthi  16840  infpn2  16846  prminf  16848  prmreclem2  16850  prmrec  16855  1arith  16860  1arith2  16861  vdwlem13  16926  ramz  16958  prmgap  16992  prmgaplcm  16993  prmgapprmo  16995  prmlem1a  17040  xpsff1o  17513  isacs1i  17601  dmaf  17999  cdaf  18000  coapm  18021  lublecllem  18313  smndex1mnd  18791  pwmnd  18818  pmtrdifel  19348  pmtrdifwrdel  19353  odf  19405  efgrelexlemb  19618  dprd2da  19912  mgpf  20071  prdscrngd  20135  cnfld1  20970  cnsubglem  20994  cnmsubglem  21008  nn0srg  21015  rge0srg  21016  pmatcoe1fsupp  22203  isbasis3g  22452  basdif0  22456  distop  22498  mretopd  22596  2ndcsep  22963  refref  23017  kqf  23251  fbssfi  23341  filconn  23387  prdstmdd  23628  ustfilxp  23717  prdsxmslem2  24038  qdensere  24286  recld2  24330  isclmi0  24614  iscvsi  24645  ovolf  24999  dyadmax  25115  dveflem  25496  mdegxrf  25586  fta1  25821  vieta1  25825  aalioulem2  25846  taylfval  25871  pilem2  25964  pilem3  25965  recosf1o  26044  divlogrlim  26143  logcn  26155  ressatans  26439  leibpi  26447  ftalem3  26579  chtub  26715  2sqlem6  26926  2sqlem10  26931  2sqreulem4  26957  chtppilim  26978  pntpbnd1  27089  pntlem3  27112  padicabvf  27134  bdayfo  27180  nodense  27195  oldf  27352  scutfo  27398  addsfo  27467  negsf  27526  negsfo  27527  axcontlem2  28223  nbgrnself  28616  vtxdginducedm1  28800  isgrpoi  29751  isvciOLD  29833  cnidOLD  29835  isnvi  29866  ipasslem8  30090  hilid  30414  hlimf  30490  shsspwh  30499  pjrni  30955  pjmf1  30969  df0op2  31005  dfiop2  31006  hoaddcomi  31025  hoaddassi  31029  hocadddiri  31032  hocsubdiri  31033  hoaddridi  31039  ho0coi  31041  hoid1i  31042  hoid1ri  31043  honegsubi  31049  hoddii  31242  lnopunilem2  31264  elunop2  31266  lnophm  31272  imaelshi  31311  cnlnadjlem8  31327  pjnmopi  31401  pjsdii  31408  pjddii  31409  pjtoi  31432  chirred  31648  nnindf  32025  nn0min  32026  wrdt2ind  32117  ccfldsrarelvec  32745  esum2d  33091  dmvlsiga  33127  volmeas  33229  ddemeas  33234  sxbrsigalem3  33271  coinfliprv  33481  ballotlem7  33534  signsw0glem  33564  rpsqrtcn  33605  tgoldbachgt  33675  bnj580  33924  bnj1384  34043  bnj1497  34071  kur14lem9  34205  sat1el2xp  34370  msrf  34533  dfon2lem7  34761  fobigcup  34872  nn0prpwlem  35207  topmeet  35249  onsucsuccmpi  35328  taupilemrplb  36201  relowlssretop  36244  ptrecube  36488  poimirlem27  36515  heicant  36523  mblfinlem1  36525  volsupnfl  36533  dvtan  36538  itg2addnc  36542  indexa  36601  sstotbnd2  36642  heiborlem7  36685  atpsubN  38624  idldil  38985  cdleme50ldil  39419  mzpclall  41465  dgraaf  41889  arearect  41964  areaquad  41965  onintunirab  41976  onsupuni  41978  infordmin  42283  omiscard  42294  clsk1indlem2  42793  clsk1indlem4  42795  mnuunid  43036  mnurndlem1  43040  prmunb2  43070  radcnvrat  43073  unirnmapsn  43913  ssmapsn  43915  upbdrech  44015  supminfxr  44174  supminfxr2  44179  supminfxrrnmpt  44181  rexanuz2nf  44203  fsumiunss  44291  resincncf  44591  dmvolss  44701  volioof  44703  stoweidlem57  44773  wallispilem3  44783  stirlinglem13  44802  dirkertrigeqlem3  44816  fourierdlem62  44884  salexct  45050  salexct3  45058  salgencntex  45059  salgensscntex  45060  gsumge0cl  45087  0ome  45245  icoresmbl  45259  hoidmv1le  45310  smflimlem1  45487  smfpimbor1lem2  45515  smfliminflem  45546  natlocalincr  45590  ralndv1  45813  fmtno4prm  46243  31prm  46265  tgoldbach  46485  nn0mnd  46589  rngmgpf  46653  pzriprnglem4  46808  pzriprnglem9  46813  pzriprnglem14  46818  2zlidl  46832  2zrngagrp  46841  2zrngnmlid  46847  crhmsubc  46976  drhmsubc  46978  drngcat  46979  fldcat  46980  fldhmsubc  46982  crhmsubcALTV  46994  drhmsubcALTV  46996  drngcatALTV  46997  fldcatALTV  46998  fldhmsubcALTV  47000  zlmodzxznm  47178  ldepsnlinc  47189  nn0sumshdiglem2  47308  itcovalpclem1  47356  itcovalt2lem1  47361  rrx2xpref1o  47404  setc2othin  47676  onsetrec  47753