Theorem mprgbir 2379

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

Syntax hints:   → wi 4   ↔ wb 98   ∈ wcel 1393  ∀wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338

This theorem depends on definitions:  df-bi 110  df-ral 2311

This theorem is referenced by:  ss2rabi  3022  rabnc  3250  ssintub  3633  tron  4119  djussxp  4481  dmiin  4580  dfco2  4820  coiun  4830  tfrlem6  5932  oacl  6040  peano1nnnn  6928  renfdisj  7079  1nn  7925  ioomax  8817  iccmax  8818  bj-omtrans2  10082