Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 equequ2 ( 𝑤 = 𝑦 → ( 𝑧 = 𝑤𝑧 = 𝑦 ) )
2 1 dvelimv ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )