Metamath Proof Explorer


Theorem sb8f

Description: Substitution of variable in universal quantifier. Version of sb8 with a disjoint variable condition, not requiring ax-10 or ax-13 . (Contributed by NM, 16-May-1993) (Revised by Wolf Lammen, 19-Jan-2023) Avoid ax-10 . (Revised by SN, 5-Dec-2024)

Ref Expression
Hypothesis sb8f.nf y φ
Assertion sb8f x φ y y x φ

Proof

Step Hyp Ref Expression
1 sb8f.nf y φ
2 sb6 y x φ x x = y φ
3 2 albii y y x φ y x x = y φ
4 alcom y x x = y φ x y x = y φ
5 sb6 x y φ y y = x φ
6 1 sbf x y φ φ
7 equcom y = x x = y
8 7 imbi1i y = x φ x = y φ
9 8 albii y y = x φ y x = y φ
10 5 6 9 3bitr3ri y x = y φ φ
11 10 albii x y x = y φ x φ
12 3 4 11 3bitrri x φ y y x φ