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 | wff ( x = y -> ph ) |