Theorem sbbibOLD 2285

Description: Obsolete version of sbbib 2369 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 2157	. . . . . 6 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
2		sbbibOLD.x	. . . . . 6 ⊢ Ⅎ𝑥𝜓
3	1, 2	nfbi 1904	. . . . 5 ⊢ Ⅎ𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓)
4	3	nf5ri 2193	. . . 4 ⊢ (([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓))
5	4	hbal 2171	. . 3 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓))
6		sbcov 2255	. . . . 5 ⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)
7		sbbibOLD.y	. . . . . 6 ⊢ Ⅎ𝑦𝜑
8	7	sbf 2268	. . . . 5 ⊢ ([𝑥 / 𝑦]𝜑 ↔ 𝜑)
9	6, 8	bitri 278	. . . 4 ⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ 𝜑)
10		spsbbi 2078	. . . 4 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜓))
11	9, 10	bitr3id 288	. . 3 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → (𝜑 ↔ [𝑥 / 𝑦]𝜓))
12	5, 11	alrimih 1825	. 2 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
13		nfs1v 2157	. . . . . 6 ⊢ Ⅎ𝑦[𝑥 / 𝑦]𝜓
14	7, 13	nfbi 1904	. . . . 5 ⊢ Ⅎ𝑦(𝜑 ↔ [𝑥 / 𝑦]𝜓)
15	14	nf5ri 2193	. . . 4 ⊢ ((𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦(𝜑 ↔ [𝑥 / 𝑦]𝜓))
16	15	hbal 2171	. . 3 ⊢ (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
17		spsbbi 2078	. . . 4 ⊢ (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑥 / 𝑦]𝜓))
18		sbcov 2255	. . . . 5 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜓 ↔ [𝑦 / 𝑥]𝜓)
19	2	sbf 2268	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓)
20	18, 19	bitri 278	. . . 4 ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜓 ↔ 𝜓)
21	17, 20	syl6bb 290	. . 3 ⊢ (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
22	16, 21	alrimih 1825	. 2 ⊢ (∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓))
23	12, 22	impbii 212	1 ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))

Syntax hints:   ↔ wb 209  ∀wal 1536  Ⅎwnf 1785  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070

This theorem is referenced by: (None)