Metamath Proof Explorer


Theorem sb8v

Description: Substitution of variable in universal quantifier. Version of sb8f with a disjoint variable condition replacing the nonfree hypothesis F/ y ph , not requiring ax-12 . (Contributed by SN, 5-Dec-2024)

Ref Expression
Assertion sb8v x φ y y x φ

Proof

Step Hyp Ref Expression
1 sb6 y x φ x x = y φ
2 1 albii y y x φ y x x = y φ
3 alcom y x x = y φ x y x = y φ
4 equcom x = y y = x
5 4 imbi1i x = y φ y = x φ
6 5 albii y x = y φ y y = x φ
7 equsv y y = x φ φ
8 6 7 bitri y x = y φ φ
9 8 albii x y x = y φ x φ
10 2 3 9 3bitrri x φ y y x φ