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 ( 𝑥 = 𝑦 → 𝜑 ) |