Theorem sneq

Description: Equality theorem for singletons. Part of Exercise 4 of TakeutiZaring p. 15. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Assertion	sneq	⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		eqeq2	⊢ ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 ↔ 𝑥 = 𝐵 ) )
2	1	abbidv	⊢ ( 𝐴 = 𝐵 → { 𝑥 ∣ 𝑥 = 𝐴 } = { 𝑥 ∣ 𝑥 = 𝐵 } )
3		df-sn	⊢ { 𝐴 } = { 𝑥 ∣ 𝑥 = 𝐴 }
4		df-sn	⊢ { 𝐵 } = { 𝑥 ∣ 𝑥 = 𝐵 }
5	2 3 4	3eqtr4g	⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐵 } )