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 ⊢ Ⅎ _ x A
spcimgf.2 ⊢ Ⅎ x ψ
spcimgf.3 ⊢ x = A → φ → ψ
Assertion spcimgf ⊢ A ∈ V → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 spcimgf.1 ⊢ Ⅎ _ x A
2 spcimgf.2 ⊢ Ⅎ x ψ
3 spcimgf.3 ⊢ x = A → φ → ψ
4 2 1 spcimgfi1 ⊢ ∀ x x = A → φ → ψ → A ∈ V → ∀ x φ → ψ
5 4 3 mpg ⊢ A ∈ V → ∀ x φ → ψ