Theorem dveeq2ALT

Description: 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.)

	Ref	Expression
Assertion	dveeq2ALT	$$⊢\neg \forall xx=y\to \left(z=y\to \forall xz=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		equequ2	$$⊢w=y\to \left(z=w\leftrightarrow z=y\right)$$
2	1	dvelimv	$$⊢\neg \forall xx=y\to \left(z=y\to \forall xz=y\right)$$