Theorem ichbi12i

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

	Ref	Expression
Hypothesis	ichbi12i.1	$$⊢\left(x=a\wedge y=b\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	ichbi12i	$$⊢\left[x\rightleftarrows y\right]\psi \leftrightarrow \left[a\rightleftarrows b\right]\chi$$

Proof

Step	Hyp	Ref	Expression
1		ichbi12i.1	$$⊢\left(x=a\wedge y=b\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		nfv	$$⊢Ⅎb\psi$$
3	2	sbco2v	$$⊢\left[v/b\right]\left[b/y\right]\psi \leftrightarrow \left[v/y\right]\psi$$
4	3	bicomi	$$⊢\left[v/y\right]\psi \leftrightarrow \left[v/b\right]\left[b/y\right]\psi$$
5	4	sbbii	$$⊢\left[a/x\right]\left[v/y\right]\psi \leftrightarrow \left[a/x\right]\left[v/b\right]\left[b/y\right]\psi$$
6		sbcom2	$$⊢\left[a/x\right]\left[v/b\right]\left[b/y\right]\psi \leftrightarrow \left[v/b\right]\left[a/x\right]\left[b/y\right]\psi$$
7	5 6	bitri	$$⊢\left[a/x\right]\left[v/y\right]\psi \leftrightarrow \left[v/b\right]\left[a/x\right]\left[b/y\right]\psi$$
8	7	sbbii	$$⊢\left[u/a\right]\left[a/x\right]\left[v/y\right]\psi \leftrightarrow \left[u/a\right]\left[v/b\right]\left[a/x\right]\left[b/y\right]\psi$$
9		nfv	$$⊢Ⅎa\psi$$
10	9	nfsbv	$$⊢Ⅎa\left[v/y\right]\psi$$
11	10	sbco2v	$$⊢\left[u/a\right]\left[a/x\right]\left[v/y\right]\psi \leftrightarrow \left[u/x\right]\left[v/y\right]\psi$$
12	1	2sbievw	$$⊢\left[a/x\right]\left[b/y\right]\psi \leftrightarrow \chi$$
13	12	2sbbii	$$⊢\left[u/a\right]\left[v/b\right]\left[a/x\right]\left[b/y\right]\psi \leftrightarrow \left[u/a\right]\left[v/b\right]\chi$$
14	8 11 13	3bitr3i	$$⊢\left[u/x\right]\left[v/y\right]\psi \leftrightarrow \left[u/a\right]\left[v/b\right]\chi$$
15		sbcom2	$$⊢\left[u/b\right]\left[a/x\right]\left[b/y\right]\psi \leftrightarrow \left[a/x\right]\left[u/b\right]\left[b/y\right]\psi$$
16	2	sbco2v	$$⊢\left[u/b\right]\left[b/y\right]\psi \leftrightarrow \left[u/y\right]\psi$$
17	16	sbbii	$$⊢\left[a/x\right]\left[u/b\right]\left[b/y\right]\psi \leftrightarrow \left[a/x\right]\left[u/y\right]\psi$$
18	15 17	bitri	$$⊢\left[u/b\right]\left[a/x\right]\left[b/y\right]\psi \leftrightarrow \left[a/x\right]\left[u/y\right]\psi$$
19	18	sbbii	$$⊢\left[v/a\right]\left[u/b\right]\left[a/x\right]\left[b/y\right]\psi \leftrightarrow \left[v/a\right]\left[a/x\right]\left[u/y\right]\psi$$
20	12	2sbbii	$$⊢\left[v/a\right]\left[u/b\right]\left[a/x\right]\left[b/y\right]\psi \leftrightarrow \left[v/a\right]\left[u/b\right]\chi$$
21	9	nfsbv	$$⊢Ⅎa\left[u/y\right]\psi$$
22	21	sbco2v	$$⊢\left[v/a\right]\left[a/x\right]\left[u/y\right]\psi \leftrightarrow \left[v/x\right]\left[u/y\right]\psi$$
23	19 20 22	3bitr3ri	$$⊢\left[v/x\right]\left[u/y\right]\psi \leftrightarrow \left[v/a\right]\left[u/b\right]\chi$$
24	14 23	bibi12i	$$⊢\left(\left[u/x\right]\left[v/y\right]\psi \leftrightarrow \left[v/x\right]\left[u/y\right]\psi \right)\leftrightarrow \left(\left[u/a\right]\left[v/b\right]\chi \leftrightarrow \left[v/a\right]\left[u/b\right]\chi \right)$$
25	24	2albii	$$⊢\forall u\forall v\left(\left[u/x\right]\left[v/y\right]\psi \leftrightarrow \left[v/x\right]\left[u/y\right]\psi \right)\leftrightarrow \forall u\forall v\left(\left[u/a\right]\left[v/b\right]\chi \leftrightarrow \left[v/a\right]\left[u/b\right]\chi \right)$$
26		dfich2	$$⊢\left[x\rightleftarrows y\right]\psi \leftrightarrow \forall u\forall v\left(\left[u/x\right]\left[v/y\right]\psi \leftrightarrow \left[v/x\right]\left[u/y\right]\psi \right)$$
27		dfich2	$$⊢\left[a\rightleftarrows b\right]\chi \leftrightarrow \forall u\forall v\left(\left[u/a\right]\left[v/b\right]\chi \leftrightarrow \left[v/a\right]\left[u/b\right]\chi \right)$$
28	25 26 27	3bitr4i	$$⊢\left[x\rightleftarrows y\right]\psi \leftrightarrow \left[a\rightleftarrows b\right]\chi$$