Theorem sbcof2 1798

Description: Version of sbco 1956 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 1796	. . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 → ∀𝑦[𝑥 / 𝑦]𝜑)
3	2	sb6f 1791	. . . . 5 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
4	1	sb6f 1791	. . . . . . 7 ⊢ ([𝑥 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → 𝜑))
5	4	imbi2i 225	. . . . . 6 ⊢ ((𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑) ↔ (𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
6	5	albii 1458	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
7	3, 6	bitri 183	. . . 4 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
8		ax-11 1494	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑))))
9		equcomi 1692	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
10	9	imim1i 60	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑥 → 𝜑) → (𝑥 = 𝑦 → 𝜑))
11	10	imim2i 12	. . . . . . . . 9 ⊢ ((𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝜑)))
12	11	pm2.43d 50	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → 𝜑))
13	12	alimi 1443	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
14	8, 13	syl6 33	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
15	14	a2i 11	. . . . 5 ⊢ ((𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
16	15	alimi 1443	. . . 4 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
17	7, 16	sylbi 120	. . 3 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
18		ax-i9 1518	. . . . 5 ⊢ ∃𝑥 𝑥 = 𝑦
19		exim 1587	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)))
20	18, 19	mpi 15	. . . 4 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → ∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑))
21		ax-ial 1522	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑦 → 𝜑))
22	21	19.9h 1631	. . . 4 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
23	20, 22	sylib 121	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
24		sb2 1755	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)
25	17, 23, 24	3syl 17	. 2 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 → [𝑦 / 𝑥]𝜑)
26		sb1 1754	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
27		simpl 108	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦)
28		19.8a 1578	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
29	27, 28	jca 304	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
30	29	eximi 1588	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
31	9	anim1i 338	. . . . . . . . 9 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑦 = 𝑥 ∧ 𝜑))
32	27, 31	jca 304	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)))
33	32	eximi 1588	. . . . . . 7 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)))
34		ax11e 1784	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
35	33, 34	syl5 32	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
36	35	imdistani 442	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
37	36	eximi 1588	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
38	26, 30, 37	3syl 17	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
39	2	sb5f 1792	. . . 4 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
40	1	sb5f 1792	. . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))
41	40	anbi2i 453	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑) ↔ (𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
42	41	exbii 1593	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
43	39, 42	bitri 183	. . 3 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
44	38, 43	sylibr 133	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥][𝑥 / 𝑦]𝜑)
45	25, 44	impbii 125	1 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1341  ∃wex 1480  [wsb 1750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-sb 1751

This theorem is referenced by:  sbid2h  1837