Metamath Proof Explorer


Theorem elequ1

Description: An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993)

Ref Expression
Assertion elequ1 x = y x z y z

Proof

Step Hyp Ref Expression
1 ax8 x = y x z y z
2 ax8 y = x y z x z
3 2 equcoms x = y y z x z
4 1 3 impbid x = y x z y z