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