Theorem sbcom 1256

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		drsb1 1173	. . . . . 6 ⊢ (∀x x = z → ([y / x][y / x]φ ↔ [y / z][y / x]φ))
2		hbae 1143	. . . . . . 7 ⊢ (∀x x = z → ∀x∀x x = z)
3		drsb1 1173	. . . . . . 7 ⊢ (∀x x = z → ([y / x]φ ↔ [y / z]φ))
4	2, 3	sbbid 1244	. . . . . 6 ⊢ (∀x x = z → ([y / x][y / x]φ ↔ [y / x][y / z]φ))
5	1, 4	bitr3d 529	. . . . 5 ⊢ (∀x x = z → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
6	5	adantr 389	. . . 4 ⊢ ((∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀z z = y)) → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
7		hbnae 1145	. . . . . . . . 9 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
8		hbnae 1145	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
9	7, 8	hban 1007	. . . . . . . 8 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → ∀z(¬ ∀x x = z ⋀ ¬ ∀x x = y))
10		hbnae 1145	. . . . . . . . . 10 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
11		hbnae 1145	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
12	10, 11	hban 1007	. . . . . . . . 9 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → ∀x(¬ ∀x x = z ⋀ ¬ ∀x x = y))
13		ax-12 966	. . . . . . . . . . 11 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z = y → ∀x z = y)))
14	13	imp 350	. . . . . . . . . 10 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (z = y → ∀x z = y))
15	14	19.20i 990	. . . . . . . . 9 ⊢ (∀x(¬ ∀x x = z ⋀ ¬ ∀x x = y) → ∀x(z = y → ∀x z = y))
16		19.21t 1113	. . . . . . . . 9 ⊢ (∀x(z = y → ∀x z = y) → (∀x(z = y → (x = y → φ)) ↔ (z = y → ∀x(x = y → φ))))
17	12, 15, 16	3syl 20	. . . . . . . 8 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (∀x(z = y → (x = y → φ)) ↔ (z = y → ∀x(x = y → φ))))
18	9, 17	albid 1102	. . . . . . 7 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀z(z = y → ∀x(x = y → φ))))
19	18	adantrr 395	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀z z = y)) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀z(z = y → ∀x(x = y → φ))))
20		hbnae 1145	. . . . . . . . . 10 ⊢ (¬ ∀z z = y → ∀x ¬ ∀z z = y)
21	10, 20	hban 1007	. . . . . . . . 9 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀z z = y) → ∀x(¬ ∀x x = z ⋀ ¬ ∀z z = y))
22		hbnae 1145	. . . . . . . . . . . 12 ⊢ (¬ ∀z z = y → ∀z ¬ ∀z z = y)
23	7, 22	hban 1007	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀z z = y) → ∀z(¬ ∀x x = z ⋀ ¬ ∀z z = y))
24		ax-12 966	. . . . . . . . . . . . . 14 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
25	24	nalequcoms 1142	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → (¬ ∀z z = y → (x = y → ∀z x = y)))
26	25	imp 350	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀z z = y) → (x = y → ∀z x = y))
27	26	19.20i 990	. . . . . . . . . . 11 ⊢ (∀z(¬ ∀x x = z ⋀ ¬ ∀z z = y) → ∀z(x = y → ∀z x = y))
28		19.21t 1113	. . . . . . . . . . 11 ⊢ (∀z(x = y → ∀z x = y) → (∀z(x = y → (z = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
29	23, 27, 28	3syl 20	. . . . . . . . . 10 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀z z = y) → (∀z(x = y → (z = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
30		bi2.04 160	. . . . . . . . . . 11 ⊢ ((z = y → (x = y → φ)) ↔ (x = y → (z = y → φ)))
31	30	albii 997	. . . . . . . . . 10 ⊢ (∀z(z = y → (x = y → φ)) ↔ ∀z(x = y → (z = y → φ)))
32	29, 31	syl5bb 531	. . . . . . . . 9 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀z z = y) → (∀z(z = y → (x = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
33	21, 32	albid 1102	. . . . . . . 8 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀z z = y) → (∀x∀z(z = y → (x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
34		alcom 1030	. . . . . . . 8 ⊢ (∀z∀x(z = y → (x = y → φ)) ↔ ∀x∀z(z = y → (x = y → φ)))
35	33, 34	syl5bb 531	. . . . . . 7 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀z z = y) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
36	35	adantrl 394	. . . . . 6 ⊢ ((¬ ∀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 529	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀z z = y)) → (∀z(z = y → ∀x(x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
38		sb4b 1222	. . . . . . 7 ⊢ (¬ ∀z z = y → ([y / z][y / x]φ ↔ ∀z(z = y → [y / x]φ)))
39		sb4b 1222	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ([y / x]φ ↔ ∀x(x = y → φ)))
40	39	imbi2d 611	. . . . . . . 8 ⊢ (¬ ∀x x = y → ((z = y → [y / x]φ) ↔ (z = y → ∀x(x = y → φ))))
41	8, 40	albid 1102	. . . . . . 7 ⊢ (¬ ∀x x = y → (∀z(z = y → [y / x]φ) ↔ ∀z(z = y → ∀x(x = y → φ))))
42	38, 41	sylan9bbr 540	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀z z = y) → ([y / z][y / x]φ ↔ ∀z(z = y → ∀x(x = y → φ))))
43	42	adantl 388	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀z z = y)) → ([y / z][y / x]φ ↔ ∀z(z = y → ∀x(x = y → φ))))
44		sb4b 1222	. . . . . . 7 ⊢ (¬ ∀x x = y → ([y / x][y / z]φ ↔ ∀x(x = y → [y / z]φ)))
45		sb4b 1222	. . . . . . . . 9 ⊢ (¬ ∀z z = y → ([y / z]φ ↔ ∀z(z = y → φ)))
46	45	imbi2d 611	. . . . . . . 8 ⊢ (¬ ∀z z = y → ((x = y → [y / z]φ) ↔ (x = y → ∀z(z = y → φ))))
47	20, 46	albid 1102	. . . . . . 7 ⊢ (¬ ∀z z = y → (∀x(x = y → [y / z]φ) ↔ ∀x(x = y → ∀z(z = y → φ))))
48	44, 47	sylan9bb 539	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀z z = y) → ([y / x][y / z]φ ↔ ∀x(x = y → ∀z(z = y → φ))))
49	48	adantl 388	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀z z = y)) → ([y / x][y / z]φ ↔ ∀x(x = y → ∀z(z = y → φ))))
50	37, 43, 49	3bitr4d 549	. . . 4 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀z z = y)) → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
51	6, 50	pm2.61ian 476	. . 3 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀z z = y) → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
52	51	ex 373	. 2 ⊢ (¬ ∀x x = y → (¬ ∀z z = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ)))
53		hbae 1143	. . . 4 ⊢ (∀x x = y → ∀z∀x x = y)
54		sbequ12 1179	. . . . 5 ⊢ (x = y → (φ ↔ [y / x]φ))
55	54	a4s 982	. . . 4 ⊢ (∀x x = y → (φ ↔ [y / x]φ))
56	53, 55	sbbid 1244	. . 3 ⊢ (∀x x = y → ([y / z]φ ↔ [y / z][y / x]φ))
57		sbequ12 1179	. . . 4 ⊢ (x = y → ([y / z]φ ↔ [y / x][y / z]φ))
58	57	a4s 982	. . 3 ⊢ (∀x x = y → ([y / z]φ ↔ [y / x][y / z]φ))
59	56, 58	bitr3d 529	. 2 ⊢ (∀x x = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
60		sbequ12 1179	. . . 4 ⊢ (z = y → ([y / x]φ ↔ [y / z][y / x]φ))
61	60	a4s 982	. . 3 ⊢ (∀z z = y → ([y / x]φ ↔ [y / z][y / x]φ))
62		hbae 1143	. . . 4 ⊢ (∀z z = y → ∀x∀z z = y)
63		sbequ12 1179	. . . . 5 ⊢ (z = y → (φ ↔ [y / z]φ))
64	63	a4s 982	. . . 4 ⊢ (∀z z = y → (φ ↔ [y / z]φ))
65	62, 64	sbbid 1244	. . 3 ⊢ (∀z z = y → ([y / x]φ ↔ [y / x][y / z]φ))
66	61, 65	bitr3d 529	. 2 ⊢ (∀z z = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
67	52, 59, 66	pm2.61ii 130	1 ⊢ ([y / z][y / x]φ ↔ [y / x][y / z]φ)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952  [wsbc 1168

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain