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	$$⊢\left\{x|x\subseteq A\right\}=\left\{y|y\subseteq A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		sseq1	$$⊢x=z\to \left(x\subseteq A\leftrightarrow z\subseteq A\right)$$
2	1	cbvabv	$$⊢\left\{x|x\subseteq A\right\}=\left\{z|z\subseteq A\right\}$$
3		sseq1	$$⊢z=y\to \left(z\subseteq A\leftrightarrow y\subseteq A\right)$$
4	3	cbvabv	$$⊢\left\{z|z\subseteq A\right\}=\left\{y|y\subseteq A\right\}$$
5	2 4	eqtri	$$⊢\left\{x|x\subseteq A\right\}=\left\{y|y\subseteq A\right\}$$