This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 2sb6 ⊢ ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜑 ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜑 ) )
2 alcom ⊢ ( ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜑 ) )
3 ancomst ⊢ ( ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜑 ) ↔ ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜑 ) )
4 3 2albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜑 ) )
5 1 2 4 3bitri ⊢ ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜑 ) )
6 2sb6 ⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜑 ) )
7 5 6 bitr4i ⊢ ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜑 ↔ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 )
8 sbequ ⊢ ( 𝑢 = 𝑦 → ( [ 𝑢 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
9 8 sbbidv ⊢ ( 𝑢 = 𝑦 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
10 7 9 bitr3id ⊢ ( 𝑢 = 𝑦 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑣 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
11 sbequ ⊢ ( 𝑣 = 𝑤 → ( [ 𝑣 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
12 10 11 sylan9bb ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
13 sbequ ⊢ ( 𝑣 = 𝑤 → ( [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑤 / 𝑧 ] 𝜑 ) )
14 13 sbbidv ⊢ ( 𝑣 = 𝑤 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑢 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
15 sbequ ⊢ ( 𝑢 = 𝑦 → ( [ 𝑢 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
16 14 15 sylan9bbr ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
17 12 16 bitr3d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
18 17 ex ⊢ ( 𝑢 = 𝑦 → ( 𝑣 = 𝑤 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) ) )
19 ax6ev ⊢ ∃ 𝑢 𝑢 = 𝑦
20 18 19 exlimiiv ⊢ ( 𝑣 = 𝑤 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
21 ax6ev ⊢ ∃ 𝑣 𝑣 = 𝑤
22 20 21 exlimiiv ⊢ ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 )