Metamath Proof Explorer


Theorem sbelx

Description: Elimination of substitution. Also see sbel2x . (Contributed by NM, 5-Aug-1993) Avoid ax-13 . (Revised by Wolf Lammen, 6-Aug-2023) Avoid ax-10 . (Revised by Gino Giotto, 20-Aug-2023)

Ref Expression
Assertion sbelx φ x x = y x y φ

Proof

Step Hyp Ref Expression
1 sbequ12r x = y x y φ φ
2 1 equsexvw x x = y x y φ φ
3 2 bicomi φ x x = y x y φ