Theorem ralsn

Description: Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009)

	Ref	Expression
Hypotheses	ralsn.1	⊢ 𝐴 ∈ V
	ralsn.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	ralsn	⊢ ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ralsn.1	⊢ 𝐴 ∈ V
2		ralsn.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3	2	ralsng	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) )
4	1 3	ax-mp	⊢ ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 )