Theorem mprgbir 2528

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

Syntax hints:   → wi 4   ↔ wb 104   ∈ wcel 2141  ∀wral 2448

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 1442

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

This theorem is referenced by:  ss2rabi  3229  rabnc  3446  ssintub  3847  tron  4365  djussxp  4754  dmiin  4855  dfco2  5108  coiun  5118  tfrlem6  6293  oacl  6437  sbthlem1  6932  peano1nnnn  7807  renfdisj  7972  1nn  8882  ioomax  9898  iccmax  9899  fxnn0nninf  10387  fisumcom2  11394  fprodcom2fi  11582  bezoutlemmain  11946  dfphi2  12167  unennn  12345  znnen  12346  istopon  12770  neipsm  12913  bj-omtrans2  13957  nninfomnilem  14016  exmidsbthrlem  14019