Theorem sbcof2 1824

Description: Version of sbco 1987 where 𝑥 is not free in 𝜑. (Contributed by Jim Kingdon, 28-Dec-2017.)

Hypothesis

Ref	Expression
sbcof2.1	⊢ (𝜑 → ∀𝑥𝜑)

Assertion

Ref	Expression
sbcof2	⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Proof of Theorem sbcof2

Step	Hyp	Ref	Expression
1		sbcof2.1	. . . . . . 7 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	hbsb3 1822	. . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 → ∀𝑦[𝑥 / 𝑦]𝜑)
3	2	sb6f 1817	. . . . 5 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
4	1	sb6f 1817	. . . . . . 7 ⊢ ([𝑥 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → 𝜑))
5	4	imbi2i 226	. . . . . 6 ⊢ ((𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑) ↔ (𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
6	5	albii 1484	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
7	3, 6	bitri 184	. . . 4 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
8		ax-11 1520	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑))))
9		equcomi 1718	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
10	9	imim1i 60	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑥 → 𝜑) → (𝑥 = 𝑦 → 𝜑))
11	10	imim2i 12	. . . . . . . . 9 ⊢ ((𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝜑)))
12	11	pm2.43d 50	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → 𝜑))
13	12	alimi 1469	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
14	8, 13	syl6 33	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
15	14	a2i 11	. . . . 5 ⊢ ((𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
16	15	alimi 1469	. . . 4 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
17	7, 16	sylbi 121	. . 3 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
18		ax-i9 1544	. . . . 5 ⊢ ∃𝑥 𝑥 = 𝑦
19		exim 1613	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)))
20	18, 19	mpi 15	. . . 4 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → ∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑))
21		ax-ial 1548	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑦 → 𝜑))
22	21	19.9h 1657	. . . 4 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
23	20, 22	sylib 122	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
24		sb2 1781	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)
25	17, 23, 24	3syl 17	. 2 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 → [𝑦 / 𝑥]𝜑)
26		sb1 1780	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
27		simpl 109	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦)
28		19.8a 1604	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
29	27, 28	jca 306	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
30	29	eximi 1614	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
31	9	anim1i 340	. . . . . . . . 9 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑦 = 𝑥 ∧ 𝜑))
32	27, 31	jca 306	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)))
33	32	eximi 1614	. . . . . . 7 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)))
34		ax11e 1810	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
35	33, 34	syl5 32	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
36	35	imdistani 445	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
37	36	eximi 1614	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
38	26, 30, 37	3syl 17	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
39	2	sb5f 1818	. . . 4 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
40	1	sb5f 1818	. . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))
41	40	anbi2i 457	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑) ↔ (𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
42	41	exbii 1619	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
43	39, 42	bitri 184	. . 3 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
44	38, 43	sylibr 134	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥][𝑥 / 𝑦]𝜑)
45	25, 44	impbii 126	1 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1362  ∃wex 1506  [wsb 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-sb 1777

This theorem is referenced by:  sbid2h  1863