Theorem mprgbir 2449

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

Syntax hints:   → wi 4   ↔ wb 104   ∈ wcel 1448  ∀wral 2375

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393

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

This theorem is referenced by:  ss2rabi  3126  rabnc  3342  ssintub  3736  tron  4242  djussxp  4622  dmiin  4723  dfco2  4974  coiun  4984  tfrlem6  6143  oacl  6286  sbthlem1  6773  peano1nnnn  7539  renfdisj  7696  1nn  8589  ioomax  9572  iccmax  9573  fxnn0nninf  10052  fisumcom2  11046  bezoutlemmain  11479  dfphi2  11688  unennn  11702  znnen  11703  istopon  11962  neipsm  12105  bj-omtrans2  12740  nninfomnilem  12798  exmidsbthrlem  12801