Theorem dveeq1-o16

Description: Version of dveeq1 using ax-c16 instead of ax-5 . (Contributed by NM, 29-Apr-2008) TODO: Recover proof from older set.mm to remove use of ax-5 . (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dveeq1-o16	$$⊢\neg \forall xx=y\to \left(y=z\to \forall xy=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax5eq	$$⊢w=z\to \forall xw=z$$
2		ax5eq	$$⊢y=z\to \forall wy=z$$
3		equequ1	$$⊢w=y\to \left(w=z\leftrightarrow y=z\right)$$
4	1 2 3	dvelimh	$$⊢\neg \forall xx=y\to \left(y=z\to \forall xy=z\right)$$