Theorem sbcof2 1669

Description: Version of sbco 1820 where x is not free in φ. (Contributed by Jim Kingdon, 28-Dec-2017.)

Hypothesis

Ref	Expression
sbcof2.1	⊢ (φ → ∀xφ)

Assertion

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

Proof of Theorem sbcof2

Step	Hyp	Ref	Expression
1		sbcof2.1	. . . . . . 7 ⊢ (φ → ∀xφ)
2	1	hbsb3 1667	. . . . . 6 ⊢ ([x / y]φ → ∀y[x / y]φ)
3	2	sb6f 1662	. . . . 5 ⊢ ([y / x][x / y]φ ↔ ∀x(x = y → [x / y]φ))
4	1	sb6f 1662	. . . . . . 7 ⊢ ([x / y]φ ↔ ∀y(y = x → φ))
5	4	imbi2i 215	. . . . . 6 ⊢ ((x = y → [x / y]φ) ↔ (x = y → ∀y(y = x → φ)))
6	5	albii 1335	. . . . 5 ⊢ (∀x(x = y → [x / y]φ) ↔ ∀x(x = y → ∀y(y = x → φ)))
7	3, 6	bitri 173	. . . 4 ⊢ ([y / x][x / y]φ ↔ ∀x(x = y → ∀y(y = x → φ)))
8		ax-11 1374	. . . . . . 7 ⊢ (x = y → (∀y(y = x → φ) → ∀x(x = y → (y = x → φ))))
9		equcomi 1570	. . . . . . . . . . 11 ⊢ (x = y → y = x)
10	9	imim1i 54	. . . . . . . . . 10 ⊢ ((y = x → φ) → (x = y → φ))
11	10	imim2i 12	. . . . . . . . 9 ⊢ ((x = y → (y = x → φ)) → (x = y → (x = y → φ)))
12	11	pm2.43d 44	. . . . . . . 8 ⊢ ((x = y → (y = x → φ)) → (x = y → φ))
13	12	alimi 1320	. . . . . . 7 ⊢ (∀x(x = y → (y = x → φ)) → ∀x(x = y → φ))
14	8, 13	syl6 29	. . . . . 6 ⊢ (x = y → (∀y(y = x → φ) → ∀x(x = y → φ)))
15	14	a2i 11	. . . . 5 ⊢ ((x = y → ∀y(y = x → φ)) → (x = y → ∀x(x = y → φ)))
16	15	alimi 1320	. . . 4 ⊢ (∀x(x = y → ∀y(y = x → φ)) → ∀x(x = y → ∀x(x = y → φ)))
17	7, 16	sylbi 114	. . 3 ⊢ ([y / x][x / y]φ → ∀x(x = y → ∀x(x = y → φ)))
18		ax-i9 1400	. . . . 5 ⊢ ∃x x = y
19		exim 1468	. . . . 5 ⊢ (∀x(x = y → ∀x(x = y → φ)) → (∃x x = y → ∃x∀x(x = y → φ)))
20	18, 19	mpi 15	. . . 4 ⊢ (∀x(x = y → ∀x(x = y → φ)) → ∃x∀x(x = y → φ))
21		ax-ial 1405	. . . . 5 ⊢ (∀x(x = y → φ) → ∀x∀x(x = y → φ))
22	21	19.9h 1512	. . . 4 ⊢ (∃x∀x(x = y → φ) ↔ ∀x(x = y → φ))
23	20, 22	sylib 127	. . 3 ⊢ (∀x(x = y → ∀x(x = y → φ)) → ∀x(x = y → φ))
24		sb2 1628	. . 3 ⊢ (∀x(x = y → φ) → [y / x]φ)
25	17, 23, 24	3syl 17	. 2 ⊢ ([y / x][x / y]φ → [y / x]φ)
26		sb1 1627	. . . 4 ⊢ ([y / x]φ → ∃x(x = y ∧ φ))
27		ax-ia1 99	. . . . . 6 ⊢ ((x = y ∧ φ) → x = y)
28		19.8a 1460	. . . . . 6 ⊢ ((x = y ∧ φ) → ∃x(x = y ∧ φ))
29	27, 28	jca 290	. . . . 5 ⊢ ((x = y ∧ φ) → (x = y ∧ ∃x(x = y ∧ φ)))
30	29	eximi 1469	. . . 4 ⊢ (∃x(x = y ∧ φ) → ∃x(x = y ∧ ∃x(x = y ∧ φ)))
31	9	anim1i 323	. . . . . . . . 9 ⊢ ((x = y ∧ φ) → (y = x ∧ φ))
32	27, 31	jca 290	. . . . . . . 8 ⊢ ((x = y ∧ φ) → (x = y ∧ (y = x ∧ φ)))
33	32	eximi 1469	. . . . . . 7 ⊢ (∃x(x = y ∧ φ) → ∃x(x = y ∧ (y = x ∧ φ)))
34		ax11e 1655	. . . . . . 7 ⊢ (x = y → (∃x(x = y ∧ (y = x ∧ φ)) → ∃y(y = x ∧ φ)))
35	33, 34	syl5 28	. . . . . 6 ⊢ (x = y → (∃x(x = y ∧ φ) → ∃y(y = x ∧ φ)))
36	35	imdistani 422	. . . . 5 ⊢ ((x = y ∧ ∃x(x = y ∧ φ)) → (x = y ∧ ∃y(y = x ∧ φ)))
37	36	eximi 1469	. . . 4 ⊢ (∃x(x = y ∧ ∃x(x = y ∧ φ)) → ∃x(x = y ∧ ∃y(y = x ∧ φ)))
38	26, 30, 37	3syl 17	. . 3 ⊢ ([y / x]φ → ∃x(x = y ∧ ∃y(y = x ∧ φ)))
39	2	sb5f 1663	. . . 4 ⊢ ([y / x][x / y]φ ↔ ∃x(x = y ∧ [x / y]φ))
40	1	sb5f 1663	. . . . . 6 ⊢ ([x / y]φ ↔ ∃y(y = x ∧ φ))
41	40	anbi2i 433	. . . . 5 ⊢ ((x = y ∧ [x / y]φ) ↔ (x = y ∧ ∃y(y = x ∧ φ)))
42	41	exbii 1474	. . . 4 ⊢ (∃x(x = y ∧ [x / y]φ) ↔ ∃x(x = y ∧ ∃y(y = x ∧ φ)))
43	39, 42	bitri 173	. . 3 ⊢ ([y / x][x / y]φ ↔ ∃x(x = y ∧ ∃y(y = x ∧ φ)))
44	38, 43	sylibr 137	. 2 ⊢ ([y / x]φ → [y / x][x / y]φ)
45	25, 44	impbii 117	1 ⊢ ([y / x][x / y]φ ↔ [y / x]φ)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1224  ∃wex 1358  [wsb 1623

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-11 1374  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405

This theorem depends on definitions:  df-bi 110  df-sb 1624

This theorem is referenced by:  sbid2h  1707