Theorem mprgbir 2591

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2202  ∀wral 2511

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 2516

This theorem is referenced by:  ss2rabi  3310  rabnc  3529  ssintub  3951  tron  4485  djussxp  4881  dmiin  4984  dfco2  5243  coiun  5253  tfrlem6  6525  oacl  6671  sbthlem1  7199  peano1nnnn  8115  renfdisj  8282  1nn  9197  ioomax  10228  iccmax  10229  xnn0nnen  10745  fxnn0nninf  10747  fisumcom2  12062  fprodcom2fi  12250  bezoutlemmain  12632  dfphi2  12855  unennn  13081  znnen  13082  istopon  14807  neipsm  14948  lgsquadlem2  15880  pw0ss  16007  clwwlkn0  16332  bj-omtrans2  16656  nninfomnilem  16727  exmidsbthrlem  16733