Theorem ichbi12i 47447

Description: Equivalence for interchangeable setvar variables. (Contributed by AV, 29-Jul-2023.)

Hypothesis

Ref	Expression
ichbi12i.1	⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ichbi12i	⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒)

Distinct variable groups:   𝑎,𝑏,𝜓   𝑥,𝑦,𝜒   𝑥,𝑎,𝑦,𝑏

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑎,𝑏)

Proof of Theorem ichbi12i

Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑏𝜓
2	1	sbco2v 2332	. . . . . . . . 9 ⊢ ([𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑦]𝜓)
3	2	bicomi 224	. . . . . . . 8 ⊢ ([𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
4	3	sbbii 2076	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
5		sbcom2 2173	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
6	4, 5	bitri 275	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
7	6	sbbii 2076	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
8		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑎𝜓
9	8	nfsbv 2330	. . . . . 6 ⊢ Ⅎ𝑎[𝑣 / 𝑦]𝜓
10	9	sbco2v 2332	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)
11		ichbi12i.1	. . . . . . 7 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒))
12	11	2sbievw 2096	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ 𝜒)
13	12	2sbbii 2077	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
14	7, 10, 13	3bitr3i 301	. . . 4 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
15		sbcom2 2173	. . . . . . 7 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓)
16	1	sbco2v 2332	. . . . . . . 8 ⊢ ([𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑦]𝜓)
17	16	sbbii 2076	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
18	15, 17	bitri 275	. . . . . 6 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
19	18	sbbii 2076	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
20	12	2sbbii 2077	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
21	8	nfsbv 2330	. . . . . 6 ⊢ Ⅎ𝑎[𝑢 / 𝑦]𝜓
22	21	sbco2v 2332	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓)
23	19, 20, 22	3bitr3ri 302	. . . 4 ⊢ ([𝑣 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
24	14, 23	bibi12i 339	. . 3 ⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
25	24	2albii 1820	. 2 ⊢ (∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
26		dfich2 47445	. 2 ⊢ ([𝑥⇄𝑦]𝜓 ↔ ∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓))
27		dfich2 47445	. 2 ⊢ ([𝑎⇄𝑏]𝜒 ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
28	25, 26, 27	3bitr4i 303	1 ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538  [wsb 2064  [wich 47432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-ich 47433

This theorem is referenced by: (None)