Metamath Proof Explorer

Theorem aev

Description: A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006) Remove dependency on ax-11 . (Revised by Wolf Lammen, 7-Sep-2018) Remove dependency on ax-13 , inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019) Remove dependency on ax-12 . (Revised by Wolf Lammen, 19-Mar-2021)

Ref Expression
Assertion aev x x = y z t = u


Step Hyp Ref Expression
1 aevlem x x = y v v = w
2 aeveq v v = w t = u
3 2 alrimiv v v = w z t = u
4 1 3 syl x x = y z t = u