Theorem sbcom 2089

Description: A commutativity law for substitution. (Contributed by NM, 27-May-1997.)

Assertion

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

Proof of Theorem sbcom

Step	Hyp	Ref	Expression
1		drsb1 2022	. . . . . 6 ⊢ (∀x x = z → ([y / x][y / x]φ ↔ [y / z][y / x]φ))
2		nfae 1954	. . . . . . 7 ⊢ Ⅎx∀x x = z
3		drsb1 2022	. . . . . . 7 ⊢ (∀x x = z → ([y / x]φ ↔ [y / z]φ))
4	2, 3	sbbid 2078	. . . . . 6 ⊢ (∀x x = z → ([y / x][y / x]φ ↔ [y / x][y / z]φ))
5	1, 4	bitr3d 246	. . . . 5 ⊢ (∀x x = z → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
6	5	adantr 451	. . . 4 ⊢ ((∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
7		nfnae 1956	. . . . . . . . 9 ⊢ Ⅎz ¬ ∀x x = z
8		nfnae 1956	. . . . . . . . 9 ⊢ Ⅎz ¬ ∀x x = y
9	7, 8	nfan 1824	. . . . . . . 8 ⊢ Ⅎz(¬ ∀x x = z ∧ ¬ ∀x x = y)
10		nfeqf 1958	. . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → Ⅎx z = y)
11		19.21t 1795	. . . . . . . . 9 ⊢ (Ⅎx z = y → (∀x(z = y → (x = y → φ)) ↔ (z = y → ∀x(x = y → φ))))
12	10, 11	syl 15	. . . . . . . 8 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (∀x(z = y → (x = y → φ)) ↔ (z = y → ∀x(x = y → φ))))
13	9, 12	albid 1772	. . . . . . 7 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀z(z = y → ∀x(x = y → φ))))
14	13	adantrr 697	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀z(z = y → ∀x(x = y → φ))))
15		alcom 1737	. . . . . . . 8 ⊢ (∀z∀x(z = y → (x = y → φ)) ↔ ∀x∀z(z = y → (x = y → φ)))
16		nfnae 1956	. . . . . . . . . 10 ⊢ Ⅎx ¬ ∀x x = z
17		nfnae 1956	. . . . . . . . . 10 ⊢ Ⅎx ¬ ∀z z = y
18	16, 17	nfan 1824	. . . . . . . . 9 ⊢ Ⅎx(¬ ∀x x = z ∧ ¬ ∀z z = y)
19		bi2.04 350	. . . . . . . . . . 11 ⊢ ((z = y → (x = y → φ)) ↔ (x = y → (z = y → φ)))
20	19	albii 1566	. . . . . . . . . 10 ⊢ (∀z(z = y → (x = y → φ)) ↔ ∀z(x = y → (z = y → φ)))
21		aecom 1946	. . . . . . . . . . . . 13 ⊢ (∀z z = x → ∀x x = z)
22	21	con3i 127	. . . . . . . . . . . 12 ⊢ (¬ ∀x x = z → ¬ ∀z z = x)
23		nfeqf 1958	. . . . . . . . . . . 12 ⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = y) → Ⅎz x = y)
24	22, 23	sylan 457	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → Ⅎz x = y)
25		19.21t 1795	. . . . . . . . . . 11 ⊢ (Ⅎz x = y → (∀z(x = y → (z = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
26	24, 25	syl 15	. . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (∀z(x = y → (z = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
27	20, 26	syl5bb 248	. . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (∀z(z = y → (x = y → φ)) ↔ (x = y → ∀z(z = y → φ))))
28	18, 27	albid 1772	. . . . . . . 8 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (∀x∀z(z = y → (x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
29	15, 28	syl5bb 248	. . . . . . 7 ⊢ ((¬ ∀x x = z ∧ ¬ ∀z z = y) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
30	29	adantrl 696	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → (∀z∀x(z = y → (x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
31	14, 30	bitr3d 246	. . . . 5 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → (∀z(z = y → ∀x(x = y → φ)) ↔ ∀x(x = y → ∀z(z = y → φ))))
32		sb4b 2054	. . . . . . 7 ⊢ (¬ ∀z z = y → ([y / z][y / x]φ ↔ ∀z(z = y → [y / x]φ)))
33		sb4b 2054	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ([y / x]φ ↔ ∀x(x = y → φ)))
34	33	imbi2d 307	. . . . . . . 8 ⊢ (¬ ∀x x = y → ((z = y → [y / x]φ) ↔ (z = y → ∀x(x = y → φ))))
35	8, 34	albid 1772	. . . . . . 7 ⊢ (¬ ∀x x = y → (∀z(z = y → [y / x]φ) ↔ ∀z(z = y → ∀x(x = y → φ))))
36	32, 35	sylan9bbr 681	. . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀z z = y) → ([y / z][y / x]φ ↔ ∀z(z = y → ∀x(x = y → φ))))
37	36	adantl 452	. . . . 5 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → ([y / z][y / x]φ ↔ ∀z(z = y → ∀x(x = y → φ))))
38		sb4b 2054	. . . . . . 7 ⊢ (¬ ∀x x = y → ([y / x][y / z]φ ↔ ∀x(x = y → [y / z]φ)))
39		sb4b 2054	. . . . . . . . 9 ⊢ (¬ ∀z z = y → ([y / z]φ ↔ ∀z(z = y → φ)))
40	39	imbi2d 307	. . . . . . . 8 ⊢ (¬ ∀z z = y → ((x = y → [y / z]φ) ↔ (x = y → ∀z(z = y → φ))))
41	17, 40	albid 1772	. . . . . . 7 ⊢ (¬ ∀z z = y → (∀x(x = y → [y / z]φ) ↔ ∀x(x = y → ∀z(z = y → φ))))
42	38, 41	sylan9bb 680	. . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀z z = y) → ([y / x][y / z]φ ↔ ∀x(x = y → ∀z(z = y → φ))))
43	42	adantl 452	. . . . 5 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → ([y / x][y / z]φ ↔ ∀x(x = y → ∀z(z = y → φ))))
44	31, 37, 43	3bitr4d 276	. . . 4 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀z z = y)) → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
45	6, 44	pm2.61ian 765	. . 3 ⊢ ((¬ ∀x x = y ∧ ¬ ∀z z = y) → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
46	45	ex 423	. 2 ⊢ (¬ ∀x x = y → (¬ ∀z z = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ)))
47		nfae 1954	. . . 4 ⊢ Ⅎz∀x x = y
48		sbequ12 1919	. . . . 5 ⊢ (x = y → (φ ↔ [y / x]φ))
49	48	sps 1754	. . . 4 ⊢ (∀x x = y → (φ ↔ [y / x]φ))
50	47, 49	sbbid 2078	. . 3 ⊢ (∀x x = y → ([y / z]φ ↔ [y / z][y / x]φ))
51		sbequ12 1919	. . . 4 ⊢ (x = y → ([y / z]φ ↔ [y / x][y / z]φ))
52	51	sps 1754	. . 3 ⊢ (∀x x = y → ([y / z]φ ↔ [y / x][y / z]φ))
53	50, 52	bitr3d 246	. 2 ⊢ (∀x x = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
54		sbequ12 1919	. . . 4 ⊢ (z = y → ([y / x]φ ↔ [y / z][y / x]φ))
55	54	sps 1754	. . 3 ⊢ (∀z z = y → ([y / x]φ ↔ [y / z][y / x]φ))
56		nfae 1954	. . . 4 ⊢ Ⅎx∀z z = y
57		sbequ12 1919	. . . . 5 ⊢ (z = y → (φ ↔ [y / z]φ))
58	57	sps 1754	. . . 4 ⊢ (∀z z = y → (φ ↔ [y / z]φ))
59	56, 58	sbbid 2078	. . 3 ⊢ (∀z z = y → ([y / x]φ ↔ [y / x][y / z]φ))
60	55, 59	bitr3d 246	. 2 ⊢ (∀z z = y → ([y / z][y / x]φ ↔ [y / x][y / z]φ))
61	46, 53, 60	pm2.61ii 157	1 ⊢ ([y / z][y / x]φ ↔ [y / x][y / z]φ)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  Ⅎwnf 1544  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by: (None)