Theorem mprgbir 2552

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2164  ∀wral 2472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460

This theorem depends on definitions:  df-bi 117  df-ral 2477

This theorem is referenced by:  ss2rabi  3261  rabnc  3479  ssintub  3888  tron  4413  djussxp  4807  dmiin  4908  dfco2  5165  coiun  5175  tfrlem6  6369  oacl  6513  sbthlem1  7016  peano1nnnn  7912  renfdisj  8079  1nn  8993  ioomax  10014  iccmax  10015  xnn0nnen  10508  fxnn0nninf  10510  fisumcom2  11581  fprodcom2fi  11769  bezoutlemmain  12135  dfphi2  12358  unennn  12554  znnen  12555  istopon  14181  neipsm  14322  bj-omtrans2  15449  nninfomnilem  15508  exmidsbthrlem  15512