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	$$⊢\neg \forall xx=y\to \left(z\in y\to \forall xz\in y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax5el	$$⊢z\in w\to \forall xz\in w$$
2		ax5el	$$⊢z\in y\to \forall wz\in y$$
3		elequ2	$$⊢w=y\to \left(z\in w\leftrightarrow z\in y\right)$$
4	1 2 3	dvelimh	$$⊢\neg \forall xx=y\to \left(z\in y\to \forall xz\in y\right)$$