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	⊢ { 𝑥 ∣ 𝑥 ⊆ 𝐴 } = { 𝑦 ∣ 𝑦 ⊆ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		sseq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴 ) )
2	1	cbvabv	⊢ { 𝑥 ∣ 𝑥 ⊆ 𝐴 } = { 𝑧 ∣ 𝑧 ⊆ 𝐴 }
3		sseq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
4	3	cbvabv	⊢ { 𝑧 ∣ 𝑧 ⊆ 𝐴 } = { 𝑦 ∣ 𝑦 ⊆ 𝐴 }
5	2 4	eqtri	⊢ { 𝑥 ∣ 𝑥 ⊆ 𝐴 } = { 𝑦 ∣ 𝑦 ⊆ 𝐴 }