Metamath Proof Explorer

Theorem naev

Description: If some set variables can assume different values, then any two distinct set variables cannot always be the same. (Contributed by Wolf Lammen, 10-Aug-2019)

Ref Expression
Assertion naev ¬ x x = y ¬ u u = v


Step Hyp Ref Expression
1 aev u u = v x x = y
2 1 con3i ¬ x x = y ¬ u u = v