Theorem dveeq2ALT

Alternate proof of dveeq2, shorter but requiring [ax-11]. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.)

Conclusion

\( \vdash \neg \forall x \, x = y \rightarrow z' = y \rightarrow \forall x \, z' = y \)

Proof

equequ2

\( \vdash w = y \rightarrow (z' = w \leftrightarrow z' = y) \)

dvelimv _