This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		ax5eq	⊢ ( 𝑤 = 𝑧 → ∀ 𝑥 𝑤 = 𝑧 )
2		ax5eq	⊢ ( 𝑦 = 𝑧 → ∀ 𝑤 𝑦 = 𝑧 )
3		equequ1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 = 𝑧 ↔ 𝑦 = 𝑧 ) )
4	1 2 3	dvelimh	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )