Theorem sbcof2 1790

Description: Version of sbco 1948 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 1788	. . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 → ∀𝑦[𝑥 / 𝑦]𝜑)
3	2	sb6f 1783	. . . . 5 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
4	1	sb6f 1783	. . . . . . 7 ⊢ ([𝑥 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → 𝜑))
5	4	imbi2i 225	. . . . . 6 ⊢ ((𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑) ↔ (𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
6	5	albii 1450	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
7	3, 6	bitri 183	. . . 4 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
8		ax-11 1486	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑))))
9		equcomi 1684	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
10	9	imim1i 60	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑥 → 𝜑) → (𝑥 = 𝑦 → 𝜑))
11	10	imim2i 12	. . . . . . . . 9 ⊢ ((𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝜑)))
12	11	pm2.43d 50	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → 𝜑))
13	12	alimi 1435	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑦 → (𝑦 = 𝑥 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
14	8, 13	syl6 33	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
15	14	a2i 11	. . . . 5 ⊢ ((𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)) → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
16	15	alimi 1435	. . . 4 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑦(𝑦 = 𝑥 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
17	7, 16	sylbi 120	. . 3 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
18		ax-i9 1510	. . . . 5 ⊢ ∃𝑥 𝑥 = 𝑦
19		exim 1579	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)))
20	18, 19	mpi 15	. . . 4 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → ∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑))
21		ax-ial 1514	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑦 → 𝜑))
22	21	19.9h 1623	. . . 4 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
23	20, 22	sylib 121	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
24		sb2 1747	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)
25	17, 23, 24	3syl 17	. 2 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 → [𝑦 / 𝑥]𝜑)
26		sb1 1746	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
27		simpl 108	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → 𝑥 = 𝑦)
28		19.8a 1570	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
29	27, 28	jca 304	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
30	29	eximi 1580	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
31	9	anim1i 338	. . . . . . . . 9 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑦 = 𝑥 ∧ 𝜑))
32	27, 31	jca 304	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)))
33	32	eximi 1580	. . . . . . 7 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)))
34		ax11e 1776	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ (𝑦 = 𝑥 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
35	33, 34	syl5 32	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
36	35	imdistani 442	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → (𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
37	36	eximi 1580	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
38	26, 30, 37	3syl 17	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
39	2	sb5f 1784	. . . 4 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
40	1	sb5f 1784	. . . . . 6 ⊢ ([𝑥 / 𝑦]𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑))
41	40	anbi2i 453	. . . . 5 ⊢ ((𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑) ↔ (𝑥 = 𝑦 ∧ ∃𝑦(𝑦 = 𝑥 ∧ 𝜑)))
42	41	exbii 1585	. . . 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 1333  ∃wex 1472  [wsb 1742

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514

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

This theorem is referenced by:  sbid2h  1829