Metamath Proof Explorer

Theorem aevlem

Description: Lemma for aev and axc16g . Change free and bound variables. Instance of aev . (Contributed by NM, 22-Jul-2015) (Proof shortened by Wolf Lammen, 17-Feb-2018) Remove dependency on ax-13 , along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019) (Revised by BJ, 29-Mar-2021)

Ref Expression
Assertion aevlem x x = y z z = t


Step Hyp Ref Expression
1 cbvaev x x = y u u = y
2 aevlem0 u u = y x x = u
3 cbvaev x x = u t t = u
4 aevlem0 t t = u z z = t
5 1 2 3 4 4syl x x = y z z = t