Metamath Proof Explorer


Theorem sb4b

Description: Simplified definition of substitution when variables are distinct. Version of sb6 with a distinctor. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 27-May-1997) Revise df-sb . (Revised by Wolf Lammen, 21-Feb-2024) (New usage is discouraged.)

Ref Expression
Assertion sb4b ¬ x x = t t x φ x x = t φ

Proof

Step Hyp Ref Expression
1 nfna1 x ¬ x x = t
2 nfeqf2 ¬ x x = t x y = t
3 1 2 nfan1 x ¬ x x = t y = t
4 equequ2 y = t x = y x = t
5 4 imbi1d y = t x = y φ x = t φ
6 5 adantl ¬ x x = t y = t x = y φ x = t φ
7 3 6 albid ¬ x x = t y = t x x = y φ x x = t φ
8 7 pm5.74da ¬ x x = t y = t x x = y φ y = t x x = t φ
9 8 albidv ¬ x x = t y y = t x x = y φ y y = t x x = t φ
10 df-sb t x φ y y = t x x = y φ
11 ax6ev y y = t
12 11 a1bi x x = t φ y y = t x x = t φ
13 19.23v y y = t x x = t φ y y = t x x = t φ
14 12 13 bitr4i x x = t φ y y = t x x = t φ
15 9 10 14 3bitr4g ¬ x x = t t x φ x x = t φ