Theorem mprgbir 3051

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 3046	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓
3		mprgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbir 231	1 ⊢ 𝜑

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

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 3045

This theorem is referenced by:  ss2rabi  4036  ssintub  4926  djussxp  5799  dmiin  5906  dfco2  6206  coiun  6217  tron  6343  onxpdisj  6448  epweon  7731  frrlem6  8247  frrlem7  8248  tfrlem6  8327  oawordeulem  8495  sbthlem1  9028  marypha2lem1  9362  ttrclselem1  9654  rankval4  9796  tcwf  9812  inlresf  9843  inrresf  9845  fin23lem16  10264  fin23lem29  10270  fin23lem30  10271  itunitc  10350  acncc  10369  wfgru  10745  renfdisj  11210  ioomax  13359  iccmax  13360  hashgval2  14319  fsumcom2  15716  fprodcom2  15926  dfphi2  16720  oppccatf  17669  dmcoass  18008  letsr  18534  smndex2dnrinv  18824  efgsf  19643  lssuni  20877  lpival  21266  cnsubdrglem  21360  retos  21560  psr1baslem  22102  istopon  22832  neips  23033  filssufilg  23831  xrhmeo  24877  iscmet3i  25245  ehlbase  25348  ovolge0  25415  unidmvol  25475  resinf1o  26478  divlogrlim  26577  dvloglem  26590  logf1o2  26592  atansssdm  26876  ppiub  27148  bday1s  27780  lrrecse  27889  clwwlkn0  30007  sspval  30702  shintcli  31308  lnopco0i  31983  imaelshi  32037  nmopadjlem  32068  nmoptrii  32073  nmopcoi  32074  nmopcoadji  32080  idleop  32110  hmopidmchi  32130  hmopidmpji  32131  djussxp2  32622  xrsclat  32995  rearchi  33310  dmvlsiga  34112  sxbrsigalem0  34255  dya2iocucvr  34268  eulerpartlemgh  34362  bnj110  34841  subfacp1lem1  35159  erdszelem2  35172  dfon2lem3  35766  filnetlem2  36360  taupi  37304  cnviun  43632  coiun1  43634  comptiunov2i  43688  cotrcltrcl  43707  cotrclrcl  43724  ssrab2f  45104  iooinlbub  45492  stirlinglem14  46078  sssalgen  46326  fvmptrabdm  47287  stgr0  47952  unilbss  48799  dfinito4  49483