Theorem ichbi12i 43667

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 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑏𝜓
2	1	sbco2v 2352	. . . . . . . . 9 ⊢ ([𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑦]𝜓)
3	2	bicomi 226	. . . . . . . 8 ⊢ ([𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
4	3	sbbii 2081	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
5		sbcom2 2168	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
6	4, 5	bitri 277	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
7	6	sbbii 2081	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
8		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑎𝜓
9	8	nfsbv 2349	. . . . . 6 ⊢ Ⅎ𝑎[𝑣 / 𝑦]𝜓
10	9	sbco2v 2352	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)
11		ichbi12i.1	. . . . . . 7 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒))
12	11	2sbievw 2105	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ 𝜒)
13	12	2sbbii 2082	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
14	7, 10, 13	3bitr3i 303	. . . 4 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
15		sbcom2 2168	. . . . . . 7 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓)
16	1	sbco2v 2352	. . . . . . . 8 ⊢ ([𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑦]𝜓)
17	16	sbbii 2081	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
18	15, 17	bitri 277	. . . . . 6 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
19	18	sbbii 2081	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
20	12	2sbbii 2082	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
21	8	nfsbv 2349	. . . . . 6 ⊢ Ⅎ𝑎[𝑢 / 𝑦]𝜓
22	21	sbco2v 2352	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓)
23	19, 20, 22	3bitr3ri 304	. . . 4 ⊢ ([𝑣 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
24	14, 23	bibi12i 342	. . 3 ⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
25	24	2albii 1821	. 2 ⊢ (∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
26		dfich2 43662	. 2 ⊢ ([𝑥⇄𝑦]𝜓 ↔ ∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓))
27		dfich2 43662	. 2 ⊢ ([𝑎⇄𝑏]𝜒 ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
28	25, 26, 27	3bitr4i 305	1 ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535  [wsb 2069  [wich 43654

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  df-ich 43655

This theorem is referenced by: (None)