Metamath Proof Explorer


Theorem sn-wcdeq

Description: Alternative to wcdeq and df-cdeq . This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq . (Contributed by SN, 26-Sep-2024) (New usage is discouraged.)

Ref Expression
Assertion sn-wcdeq x = y φ