Theorem snjust

Description: Soundness justification theorem for df-sn . (Contributed by Rodolfo Medina, 28-Apr-2010) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	snjust	|- { x | x = A } = { y | y = A }

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( x = z -> ( x = A <-> z = A ) )
2	1	cbvabv	|- { x | x = A } = { z | z = A }
3		eqeq1	|- ( z = y -> ( z = A <-> y = A ) )
4	3	cbvabv	|- { z | z = A } = { y | y = A }
5	2 4	eqtri	|- { x | x = A } = { y | y = A }