Theorem mprgbir 2535

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2148  ∀wral 2455

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 1449

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

This theorem is referenced by:  ss2rabi  3237  rabnc  3455  ssintub  3862  tron  4382  djussxp  4772  dmiin  4873  dfco2  5128  coiun  5138  tfrlem6  6316  oacl  6460  sbthlem1  6955  peano1nnnn  7850  renfdisj  8016  1nn  8929  ioomax  9947  iccmax  9948  fxnn0nninf  10437  fisumcom2  11445  fprodcom2fi  11633  bezoutlemmain  11998  dfphi2  12219  unennn  12397  znnen  12398  istopon  13483  neipsm  13624  bj-omtrans2  14679  nninfomnilem  14737  exmidsbthrlem  14740