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  3447  ssintub  3849  tron  4367  djussxp  4756  dmiin  4857  dfco2  5110  coiun  5120  tfrlem6  6295  oacl  6439  sbthlem1  6934  peano1nnnn  7814  renfdisj  7979  1nn  8889  ioomax  9905  iccmax  9906  fxnn0nninf  10394  fisumcom2  11401  fprodcom2fi  11589  bezoutlemmain  11953  dfphi2  12174  unennn  12352  znnen  12353  istopon  12805  neipsm  12948  bj-omtrans2  13992  nninfomnilem  14051  exmidsbthrlem  14054