Theorem ichbi12i 44912

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 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑏𝜓
2	1	sbco2v 2327	. . . . . . . . 9 ⊢ ([𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑦]𝜓)
3	2	bicomi 223	. . . . . . . 8 ⊢ ([𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
4	3	sbbii 2079	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓)
5		sbcom2 2161	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
6	4, 5	bitri 274	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
7	6	sbbii 2079	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓)
8		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑎𝜓
9	8	nfsbv 2324	. . . . . 6 ⊢ Ⅎ𝑎[𝑣 / 𝑦]𝜓
10	9	sbco2v 2327	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑎 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)
11		ichbi12i.1	. . . . . . 7 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒))
12	11	2sbievw 2097	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ 𝜒)
13	12	2sbbii 2080	. . . . 5 ⊢ ([𝑢 / 𝑎][𝑣 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
14	7, 10, 13	3bitr3i 301	. . . 4 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑢 / 𝑎][𝑣 / 𝑏]𝜒)
15		sbcom2 2161	. . . . . . 7 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓)
16	1	sbco2v 2327	. . . . . . . 8 ⊢ ([𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑢 / 𝑦]𝜓)
17	16	sbbii 2079	. . . . . . 7 ⊢ ([𝑎 / 𝑥][𝑢 / 𝑏][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
18	15, 17	bitri 274	. . . . . 6 ⊢ ([𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
19	18	sbbii 2079	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓)
20	12	2sbbii 2080	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑢 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
21	8	nfsbv 2324	. . . . . 6 ⊢ Ⅎ𝑎[𝑢 / 𝑦]𝜓
22	21	sbco2v 2327	. . . . 5 ⊢ ([𝑣 / 𝑎][𝑎 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓)
23	19, 20, 22	3bitr3ri 302	. . . 4 ⊢ ([𝑣 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒)
24	14, 23	bibi12i 340	. . 3 ⊢ (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
25	24	2albii 1823	. 2 ⊢ (∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓) ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
26		dfich2 44910	. 2 ⊢ ([𝑥⇄𝑦]𝜓 ↔ ∀𝑢∀𝑣([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜓))
27		dfich2 44910	. 2 ⊢ ([𝑎⇄𝑏]𝜒 ↔ ∀𝑢∀𝑣([𝑢 / 𝑎][𝑣 / 𝑏]𝜒 ↔ [𝑣 / 𝑎][𝑢 / 𝑏]𝜒))
28	25, 26, 27	3bitr4i 303	1 ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537  [wsb 2067  [wich 44897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-ich 44898

This theorem is referenced by: (None)