Theorem mprgbir 2602

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2205  ∀wral 2522

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 1498

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

This theorem is referenced by:  ss2rabi  3322  rabnc  3543  ssintub  3969  tron  4505  djussxp  4902  dmiin  5005  dfco2  5264  coiun  5274  tfrlem6  6549  oacl  6695  sbthlem1  7229  peano1nnnn  8169  renfdisj  8335  1nn  9250  ioomax  10284  iccmax  10285  xnn0nnen  10803  fxnn0nninf  10805  fisumcom2  12128  fprodcom2fi  12316  bezoutlemmain  12698  dfphi2  12921  unennn  13165  znnen  13166  istopon  14895  neipsm  15036  lgsquadlem2  15968  pw0ss  16095  clwwlkn0  16420  bj-omtrans2  16744  nninfomnilem  16813  exmidsbthrlem  16819