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	spcimgft	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) ) )
5	4 3	mpg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) )