Metamath Proof Explorer


Theorem sb2

Description: One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition ( sb6 ) or a nonfreeness hypothesis ( sb6f ). Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 13-May-1993) Revise df-sb . (Revised by Wolf Lammen, 26-Jul-2023) (New usage is discouraged.)

Ref Expression
Assertion sb2 x x = y φ y x φ

Proof

Step Hyp Ref Expression
1 pm2.27 x = y x = y φ φ
2 1 al2imi x x = y x x = y φ x φ
3 stdpc4 x φ y x φ
4 2 3 syl6 x x = y x x = y φ y x φ
5 sb4b ¬ x x = y y x φ x x = y φ
6 5 biimprd ¬ x x = y x x = y φ y x φ
7 4 6 pm2.61i x x = y φ y x φ