Theorem pwjust

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

	Ref	Expression
Assertion	pwjust	|- { x | x C_ A } = { y | y C_ A }

Proof

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