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

Metamath Proof Explorer

Theorem spcgf

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of Quine p. 44. (Contributed by NM, 2-Feb-1997) (Revised by Andrew Salmon, 12-Aug-2011)

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

Proof

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