Theorem sbbibOLD 2289

Description: Obsolete version of sbbib 2380 as of 4-Sep-2023. (Contributed by AV, 6-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
sbbibOLD.y	⊢ Ⅎ𝑦𝜑
sbbibOLD.x	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
sbbibOLD	⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbbibOLD

Step	Hyp	Ref	Expression
1		nfs1v 2160	. . . . . 6 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
2		sbbibOLD.x	. . . . . 6 ⊢ Ⅎ𝑥𝜓
3	1, 2	nfbi 1904	. . . . 5 ⊢ Ⅎ𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓)
4	3	nf5ri 2195	. . . 4 ⊢ (([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓))
5	4	hbal 2174	. . 3 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓))
6		sbcov 2258	. . . . 5 ⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)
7		sbbibOLD.y	. . . . . 6 ⊢ Ⅎ𝑦𝜑
8	7	sbf 2271	. . . . 5 ⊢ ([𝑥 / 𝑦]𝜑 ↔ 𝜑)
9	6, 8	bitri 277	. . . 4 ⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ 𝜑)
10		spsbbi 2078	. . . 4 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜓))
11	9, 10	syl5bbr 287	. . 3 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → (𝜑 ↔ [𝑥 / 𝑦]𝜓))
12	5, 11	alrimih 1824	. 2 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
13		nfs1v 2160	. . . . . 6 ⊢ Ⅎ𝑦[𝑥 / 𝑦]𝜓
14	7, 13	nfbi 1904	. . . . 5 ⊢ Ⅎ𝑦(𝜑 ↔ [𝑥 / 𝑦]𝜓)
15	14	nf5ri 2195	. . . 4 ⊢ ((𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦(𝜑 ↔ [𝑥 / 𝑦]𝜓))
16	15	hbal 2174	. . 3 ⊢ (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
17		spsbbi 2078	. . . 4 ⊢ (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑥 / 𝑦]𝜓))
18		sbcov 2258	. . . . 5 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜓 ↔ [𝑦 / 𝑥]𝜓)
19	2	sbf 2271	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
20	18, 19	bitri 277	. . . 4 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜓 ↔ 𝜓)
21	17, 20	syl6bb 289	. . 3 ⊢ (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
22	16, 21	alrimih 1824	. 2 ⊢ (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓))
23	12, 22	impbii 211	1 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))

Syntax hints:   ↔ wb 208  ∀wal 1535  Ⅎwnf 1784  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070

This theorem is referenced by: (None)