Theorem mprgbir 2488

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

Syntax hints:   → wi 4   ↔ wb 104   ∈ wcel 1480  ∀wral 2414

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

This theorem depends on definitions:  df-bi 116  df-ral 2419

This theorem is referenced by:  ss2rabi  3174  rabnc  3390  ssintub  3784  tron  4299  djussxp  4679  dmiin  4780  dfco2  5033  coiun  5043  tfrlem6  6206  oacl  6349  sbthlem1  6838  peano1nnnn  7653  renfdisj  7817  1nn  8724  ioomax  9724  iccmax  9725  fxnn0nninf  10204  fisumcom2  11200  bezoutlemmain  11675  dfphi2  11885  unennn  11899  znnen  11900  istopon  12169  neipsm  12312  bj-omtrans2  13144  nninfomnilem  13203  exmidsbthrlem  13206