Theorem ichbi12i 44528

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 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑏𝜓
2	1	sbco2v 2333	. . . . . . . . 9 ⊢ ([𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑦]𝜓)
3	2	bicomi 227	. . . . . . . 8 ⊢ ([𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
4	3	sbbii 2084	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
5		sbcom2 2167	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
6	4, 5	bitri 278	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
7	6	sbbii 2084	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
8		nfv 1922	. . . . . . 7 ⊢ Ⅎ𝑎𝜓
9	8	nfsbv 2331	. . . . . 6 ⊢ Ⅎ𝑎[𝑣 / 𝑦]𝜓
10	9	sbco2v 2333	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)
11		ichbi12i.1	. . . . . . 7 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒))
12	11	2sbievw 2103	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ 𝜒)
13	12	2sbbii 2085	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
14	7, 10, 13	3bitr3i 304	. . . 4 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
15		sbcom2 2167	. . . . . . 7 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓)
16	1	sbco2v 2333	. . . . . . . 8 ⊢ ([𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑦]𝜓)
17	16	sbbii 2084	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
18	15, 17	bitri 278	. . . . . 6 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
19	18	sbbii 2084	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
20	12	2sbbii 2085	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
21	8	nfsbv 2331	. . . . . 6 ⊢ Ⅎ𝑎[𝑢 / 𝑦]𝜓
22	21	sbco2v 2333	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓)
23	19, 20, 22	3bitr3ri 305	. . . 4 ⊢ ([𝑣 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
24	14, 23	bibi12i 343	. . 3 ⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
25	24	2albii 1828	. 2 ⊢ (∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
26		dfich2 44526	. 2 ⊢ ([𝑥⇄𝑦]𝜓 ↔ ∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓))
27		dfich2 44526	. 2 ⊢ ([𝑎⇄𝑏]𝜒 ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
28	25, 26, 27	3bitr4i 306	1 ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541  [wsb 2072  [wich 44513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-10 2143  ax-11 2160  ax-12 2177

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2073  df-ich 44514

This theorem is referenced by: (None)