This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem spcimgf

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of Quine p. 44. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses spcimgf.1 ⊢ Ⅎ 𝑥 𝐴
spcimgf.2 ⊢ Ⅎ 𝑥 𝜓
spcimgf.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) )
Assertion spcimgf ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) )

Proof

Step Hyp Ref Expression
1 spcimgf.1 ⊢ Ⅎ 𝑥 𝐴
2 spcimgf.2 ⊢ Ⅎ 𝑥 𝜓
3 spcimgf.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) )
4 2 1 spcimgfi1 ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) ) )
5 4 3 mpg ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) )