Metamath Proof Explorer

Theorem dveel2ALT

Description: Alternate proof of dveel2 using ax-c16 instead of ax-5 . (Contributed by NM, 10-May-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dveel2ALT ¬ x x = y z y x z y


Step Hyp Ref Expression
1 ax5el z w x z w
2 ax5el z y w z y
3 elequ2 w = y z w z y
4 1 2 3 dvelimh ¬ x x = y z y x z y