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  3324  rabnc  3545  ssintub  3972  tron  4508  djussxp  4905  dmiin  5008  dfco2  5267  coiun  5277  tfrlem6  6560  oacl  6706  sbthlem1  7240  peano1nnnn  8183  renfdisj  8349  1nn  9265  ioomax  10300  iccmax  10301  xnn0nnen  10823  fxnn0nninf  10825  fisumcom2  12149  fprodcom2fi  12337  bezoutlemmain  12719  dfphi2  12942  unennn  13232  znnen  13233  istopon  15004  neipsm  15145  lgsquadlem2  16077  pw0ss  16204  clwwlkn0  16529  bj-omtrans2  16853  nninfomnilem  16922  exmidsbthrlem  16928