Metamath Proof Explorer


Theorem bj-dfsb2

Description: Alternate (dual) definition of substitution df-sb not using dummy variables. (Contributed by BJ, 19-Mar-2021)

Ref Expression
Assertion bj-dfsb2 y x φ x x = y φ x = y φ

Proof

Step Hyp Ref Expression
1 dfsb1 y x φ x = y φ x x = y φ
2 bj-sbsb x = y φ x x = y φ x x = y φ x = y φ
3 1 2 bitri y x φ x x = y φ x = y φ