Theorem mprgbir 2608

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  ss2rabi  3330  rabnc  3555  ssintub  3988  tron  4527  djussxp  4925  dmiin  5028  dfco2  5287  coiun  5297  tfrlem6  6587  oacl  6733  sbthlem1  7274  peano1nnnn  8220  renfdisj  8386  1nn  9318  ioomax  10361  iccmax  10362  xnn0nnen  10889  fxnn0nninf  10891  fisumcom2  12224  fprodcom2fi  12412  bezoutlemmain  12794  dfphi2  13021  unennn  13340  znnen  13341  istopon  15205  neipsm  15346  ppiqub  16254  lgsquadlem2  16363  pw0ss  16490  clwwlkn0  16815  bj-omtrans2  17149  nninfomnilem  17227  exmidsbthrlem  17233  rirrdisj  17251