Metamath Proof Explorer

Theorem sbcom2

Description: Commutativity law for substitution. Used in proof of Theorem 9.7 of Megill p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997) (Proof shortened by Wolf Lammen, 23-Dec-2022)

Ref Expression
Assertion sbcom2 ⊢ w z y x φ ↔ y x w z φ

Proof

Step Hyp Ref Expression
1 2sb6 ⊢ v z u x φ ↔ ∀ z ∀ x z = v ∧ x = u → φ
2 alcom ⊢ ∀ z ∀ x z = v ∧ x = u → φ ↔ ∀ x ∀ z z = v ∧ x = u → φ
3 ancomst ⊢ z = v ∧ x = u → φ ↔ x = u ∧ z = v → φ
4 3 2albii ⊢ ∀ x ∀ z z = v ∧ x = u → φ ↔ ∀ x ∀ z x = u ∧ z = v → φ
5 1 2 4 3bitri ⊢ v z u x φ ↔ ∀ x ∀ z x = u ∧ z = v → φ
6 2sb6 ⊢ u x v z φ ↔ ∀ x ∀ z x = u ∧ z = v → φ
7 5 6 bitr4i ⊢ v z u x φ ↔ u x v z φ
8 sbequ ⊢ u = y → u x φ ↔ y x φ
9 8 sbbidv ⊢ u = y → v z u x φ ↔ v z y x φ
10 7 9 bitr3id ⊢ u = y → u x v z φ ↔ v z y x φ
11 sbequ ⊢ v = w → v z y x φ ↔ w z y x φ
12 10 11 sylan9bb ⊢ u = y ∧ v = w → u x v z φ ↔ w z y x φ
13 sbequ ⊢ v = w → v z φ ↔ w z φ
14 13 sbbidv ⊢ v = w → u x v z φ ↔ u x w z φ
15 sbequ ⊢ u = y → u x w z φ ↔ y x w z φ
16 14 15 sylan9bbr ⊢ u = y ∧ v = w → u x v z φ ↔ y x w z φ
17 12 16 bitr3d ⊢ u = y ∧ v = w → w z y x φ ↔ y x w z φ
18 17 ex ⊢ u = y → v = w → w z y x φ ↔ y x w z φ
19 ax6ev ⊢ ∃ u u = y
20 18 19 exlimiiv ⊢ v = w → w z y x φ ↔ y x w z φ
21 ax6ev ⊢ ∃ v v = w
22 20 21 exlimiiv ⊢ w z y x φ ↔ y x w z φ