Theorem mprgbir 3052

Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)

Hypotheses

Ref	Expression
mprgbir.1	⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
mprgbir.2	⊢ (𝑥 ∈ 𝐴 → 𝜓)

Assertion

Ref	Expression
mprgbir	⊢ 𝜑

Proof of Theorem mprgbir

Step	Hyp	Ref	Expression
1		mprgbir.2	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝜓)
2	1	rgen 3047	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓
3		mprgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbir 231	1 ⊢ 𝜑

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∀wral 3045

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

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

This theorem is referenced by:  ss2rabi  4043  ssintub  4933  djussxp  5812  dmiin  5920  dfco2  6221  coiun  6232  tron  6358  onxpdisj  6463  epweon  7754  frrlem6  8273  frrlem7  8274  tfrlem6  8353  oawordeulem  8521  sbthlem1  9057  marypha2lem1  9393  ttrclselem1  9685  rankval4  9827  tcwf  9843  inlresf  9874  inrresf  9876  fin23lem16  10295  fin23lem29  10301  fin23lem30  10302  itunitc  10381  acncc  10400  wfgru  10776  renfdisj  11241  ioomax  13390  iccmax  13391  hashgval2  14350  fsumcom2  15747  fprodcom2  15957  dfphi2  16751  oppccatf  17696  dmcoass  18035  letsr  18559  smndex2dnrinv  18849  efgsf  19666  lssuni  20852  lpival  21241  cnsubdrglem  21342  retos  21534  psr1baslem  22076  istopon  22806  neips  23007  filssufilg  23805  xrhmeo  24851  iscmet3i  25219  ehlbase  25322  ovolge0  25389  unidmvol  25449  resinf1o  26452  divlogrlim  26551  dvloglem  26564  logf1o2  26566  atansssdm  26850  ppiub  27122  bday1s  27750  lrrecse  27856  clwwlkn0  29964  sspval  30659  shintcli  31265  lnopco0i  31940  imaelshi  31994  nmopadjlem  32025  nmoptrii  32030  nmopcoi  32031  nmopcoadji  32037  idleop  32067  hmopidmchi  32087  hmopidmpji  32088  djussxp2  32579  xrsclat  32956  rearchi  33324  dmvlsiga  34126  sxbrsigalem0  34269  dya2iocucvr  34282  eulerpartlemgh  34376  bnj110  34855  subfacp1lem1  35173  erdszelem2  35186  dfon2lem3  35780  filnetlem2  36374  taupi  37318  cnviun  43646  coiun1  43648  comptiunov2i  43702  cotrcltrcl  43721  cotrclrcl  43738  ssrab2f  45118  iooinlbub  45506  stirlinglem14  46092  sssalgen  46340  fvmptrabdm  47298  stgr0  47963  unilbss  48810  dfinito4  49494