Metamath Proof Explorer


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|xA=y|yA

Proof

Step Hyp Ref Expression
1 sseq1 x=zxAzA
2 1 cbvabv x|xA=z|zA
3 sseq1 z=yzAyA
4 3 cbvabv z|zA=y|yA
5 2 4 eqtri x|xA=y|yA