Theorem ichbi12i 48542

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 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑏𝜓
2	1	sbco2v 2361	. . . . . . . . 9 ⊢ ([𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑦]𝜓)
3	2	bicomi 227	. . . . . . . 8 ⊢ ([𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
4	3	sbbii 2112	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
5		sbcom2 2208	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
6	4, 5	bitri 278	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
7	6	sbbii 2112	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
8		nfv 1946	. . . . . . 7 ⊢ Ⅎ𝑎𝜓
9	8	nfsbv 2360	. . . . . 6 ⊢ Ⅎ𝑎[𝑣 / 𝑦]𝜓
10	9	sbco2v 2361	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)
11		ichbi12i.1	. . . . . . 7 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒))
12	11	2sbievw 2132	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ 𝜒)
13	12	2sbbii 2113	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
14	7, 10, 13	3bitr3i 304	. . . 4 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
15		sbcom2 2208	. . . . . . 7 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓)
16	1	sbco2v 2361	. . . . . . . 8 ⊢ ([𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑦]𝜓)
17	16	sbbii 2112	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
18	15, 17	bitri 278	. . . . . 6 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
19	18	sbbii 2112	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
20	12	2sbbii 2113	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
21	8	nfsbv 2360	. . . . . 6 ⊢ Ⅎ𝑎[𝑢 / 𝑦]𝜓
22	21	sbco2v 2361	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓)
23	19, 20, 22	3bitr3ri 305	. . . 4 ⊢ ([𝑣 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
24	14, 23	bibi12i 342	. . 3 ⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
25	24	2albii 1852	. 2 ⊢ (∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
26		dfich2 48540	. 2 ⊢ ([𝑥⇄𝑦]𝜓 ↔ ∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓))
27		dfich2 48540	. 2 ⊢ ([𝑎⇄𝑏]𝜒 ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
28	25, 26, 27	3bitr4i 306	1 ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  [wsb 2098  [wich 48527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-ich 48528

This theorem is used by: (None)