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

Metamath Proof Explorer

Theorem dveeq2

Description: Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (Revised by NM, 20-Jul-2015) Remove dependency on ax-11 . (Revised by Wolf Lammen, 8-Sep-2018) (New usage is discouraged.)

Ref Expression
Assertion dveeq2 ⊢ ¬ ∀ x x = y → z = y → ∀ x z = y

Proof

Step Hyp Ref Expression
1 nfeqf2 ⊢ ¬ ∀ x x = y → Ⅎ x z = y
2 1 nf5rd ⊢ ¬ ∀ x x = y → z = y → ∀ x z = y