Theorem sbcom 916

Description: A commutativity law for substitution.

Assertion

Ref	Expression
sbcom	⊢ ([y / z][y / x]φ ↔ [y / x][y / z]φ)

Proof of Theorem sbcom

Step	Hyp	Ref	Expression
1		del43b 857	. . . . . 6 ⊢ (∀x x = z → ([y / x][y / x]φ ↔ [y / z][y / x]φ))
2		eq5 824	. . . . . . 7 ⊢ (∀x x = z → ∀x∀x x = z)
3		del43b 857	. . . . . . 7 ⊢ (∀x x = z → ([y / x]φ ↔ [y / z]φ))
4	2, 3	bisbd 897	. . . . . 6 ⊢ (∀x x = z → ([y / x][y / x]φ ↔ [y / x][y / z]φ))
5	1, 4	bitr3d 408	. . . . 5 ⊢ (∀x x = z → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
6	5	a1d 14	. . . 4 ⊢ (∀x x = z → ((¬ ∀x x = y ∧ ¬ ∀z z = y) → ([y / z][y / x]φ ↔ [y / x][y / z]φ)))
7		eq6 826	. . . . . . . . . 10 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
8		eq6 826	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
9	7, 8	hban 704	. . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → ∀z(¬ ∀x x = z ∧ ¬ ∀x x = y))
10		eq6 826	. . . . . . . . . . 11 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
11		eq6 826	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
12	10, 11	hban 704	. . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → ∀x(¬ ∀x x = z ∧ ¬ ∀x x = y))
13		ax-12 802	. . . . . . . . . . . 12 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z = y → ∀x z = y)))
14	13	imp 277	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (z = y → ∀x z = y))
15	14	19.20i 691	. . . . . . . . . 10 ⊢ (∀x(¬ ∀x x = z ∧ ¬ ∀x x = y) → ∀x(z = y → ∀x z = y))
16		19.21g 792	. . . . . . . . . 10 ⊢ (∀x(z = y → ∀x z = y) → (∀x(z = y → (x = y → φ)) ↔ (z = y → ∀x(x = y → φ))))
17	12, 15, 16	3syl 21	. . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (∀x(z = y → (x = y → φ)) ↔ (z = y → ∀x(x = y → φ))))
18	9, 17	biald 782	. . . . . . . 8 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀z(z = y → ∀x(x = y → φ))))
19	18	adantrr 312	. . . . . . 7 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀z(z = y → ∀x(x = y → φ))))
20		eq6 826	. . . . . . . . . . 11 ⊢ (¬ ∀z z = y → ∀x ¬ ∀z z = y)
21	10, 20	hban 704	. . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → ∀x(¬ ∀x x = z ∧ ¬ ∀z z = y))
22		eq6 826	. . . . . . . . . . . . 13 ⊢ (¬ ∀z z = y → ∀z ¬ ∀z z = y)
23	7, 22	hban 704	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → ∀z(¬ ∀x x = z ∧ ¬ ∀z z = y))
24		ax-12 802	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
25	24	eq4ds 823	. . . . . . . . . . . . . 14 ⊢ (¬ ∀x x = z → (¬ ∀z z = y → (x = y → ∀z x = y)))
26	25	imp 277	. . . . . . . . . . . . 13 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (x = y → ∀z x = y))
27	26	19.20i 691	. . . . . . . . . . . 12 ⊢ (∀z(¬ ∀x x = z ∧ ¬ ∀z z = y) → ∀z(x = y → ∀z x = y))
28		19.21g 792	. . . . . . . . . . . 12 ⊢ (∀z(x = y → ∀z x = y) → (∀z(x = y → (z = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
29	23, 27, 28	3syl 21	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (∀z(x = y → (z = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
30		bi2.04 141	. . . . . . . . . . . 12 ⊢ ((z = y → (x = y → φ)) ↔ (x = y → (z = y → φ)))
31	30	bial 695	. . . . . . . . . . 11 ⊢ (∀z(z = y → (x = y → φ)) ↔ ∀z(x = y → (z = y → φ)))
32	29, 31	syl5bb 410	. . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (∀z(z = y → (x = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
33	21, 32	biald 782	. . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (∀x∀z(z = y → (x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
34		alcom 715	. . . . . . . . 9 ⊢ (∀z∀x(z = y → (x = y → φ)) ↔ ∀x∀z(z = y → (x = y → φ)))
35	33, 34	syl5bb 410	. . . . . . . 8 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
36	35	adantrl 311	. . . . . . 7 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
37	19, 36	bitr3d 408	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → (∀z(z = y → ∀x(x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
38		sb4b 862	. . . . . . . 8 ⊢ (¬ ∀z z = y → ([y / z][y / x]φ ↔ ∀z(z = y → [y / x]φ)))
39		sb4b 862	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → ([y / x]φ ↔ ∀x(x = y → φ)))
40	39	imbi2d 464	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ((z = y → [y / x]φ) ↔ (z = y → ∀x(x = y → φ))))
41	8, 40	biald 782	. . . . . . . 8 ⊢ (¬ ∀x x = y → (∀z(z = y → [y / x]φ) ↔ ∀z(z = y → ∀x(x = y → φ))))
42	38, 41	sylan9bbr 419	. . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀z z = y) → ([y / z][y / x]φ ↔ ∀z(z = y → ∀x(x = y → φ))))
43	42	adantl 305	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → ([y / z][y / x]φ ↔ ∀z(z = y → ∀x(x = y → φ))))
44		sb4b 862	. . . . . . . 8 ⊢ (¬ ∀x x = y → ([y / x][y / z]φ ↔ ∀x(x = y → [y / z]φ)))
45		sb4b 862	. . . . . . . . . 10 ⊢ (¬ ∀z z = y → ([y / z]φ ↔ ∀z(z = y → φ)))
46	45	imbi2d 464	. . . . . . . . 9 ⊢ (¬ ∀z z = y → ((x = y → [y / z]φ) ↔ (x = y → ∀z(z = y → φ))))
47	20, 46	biald 782	. . . . . . . 8 ⊢ (¬ ∀z z = y → (∀x(x = y → [y / z]φ) ↔ ∀x(x = y → ∀z(z = y → φ))))
48	44, 47	sylan9bb 418	. . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀z z = y) → ([y / x][y / z]φ ↔ ∀x(x = y → ∀z(z = y → φ))))
49	48	adantl 305	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → ([y / x][y / z]φ ↔ ∀x(x = y → ∀z(z = y → φ))))
50	37, 43, 49	3bitr4d 424	. . . . 5 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
51	50	exp 291	. . . 4 ⊢ (¬ ∀x x = z → ((¬ ∀x x = y ∧ ¬ ∀z z = y) → ([y / z][y / x]φ ↔ [y / x][y / z]φ)))
52	6, 51	pm2.61i 110	. . 3 ⊢ ((¬ ∀x x = y ∧ ¬ ∀z z = y) → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
53	52	exp 291	. 2 ⊢ (¬ ∀x x = y → (¬ ∀z z = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ)))
54		eq5 824	. . . 4 ⊢ (∀x x = y → ∀z∀x x = y)
55		sbequ12 865	. . . . 5 ⊢ (x = y → (φ ↔ [y / x]φ))
56	55	a4s 682	. . . 4 ⊢ (∀x x = y → (φ ↔ [y / x]φ))
57	54, 56	bisbd 897	. . 3 ⊢ (∀x x = y → ([y / z]φ ↔ [y / z][y / x]φ))
58		sbequ12 865	. . . 4 ⊢ (x = y → ([y / z]φ ↔ [y / x][y / z]φ))
59	58	a4s 682	. . 3 ⊢ (∀x x = y → ([y / z]φ ↔ [y / x][y / z]φ))
60	57, 59	bitr3d 408	. 2 ⊢ (∀x x = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
61		sbequ12 865	. . . 4 ⊢ (z = y → ([y / x]φ ↔ [y / z][y / x]φ))
62	61	a4s 682	. . 3 ⊢ (∀z z = y → ([y / x]φ ↔ [y / z][y / x]φ))
63		eq5 824	. . . 4 ⊢ (∀z z = y → ∀x∀z z = y)
64		sbequ12 865	. . . . 5 ⊢ (z = y → (φ ↔ [y / z]φ))
65	64	a4s 682	. . . 4 ⊢ (∀z z = y → (φ ↔ [y / z]φ))
66	63, 65	bisbd 897	. . 3 ⊢ (∀z z = y → ([y / x]φ ↔ [y / x][y / z]φ))
67	62, 66	bitr3d 408	. 2 ⊢ (∀z z = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
68	53, 60, 67	pm2.61ii 113	1 ⊢ ([y / z][y / x]φ ↔ [y / x][y / z]φ)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672   = weq 797  [wsb 852

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org