Theorem icheq

Description: In an equality of setvar variables, the setvar variables are interchangeable. (Contributed by AV, 29-Jul-2023)

	Ref	Expression
Assertion	icheq	$$⊢\left[x\rightleftarrows y\right]x=y$$

Proof

Step	Hyp	Ref	Expression
1		equsb3r	$$⊢\left[z/y\right]x=y\leftrightarrow x=z$$
2	1	2sbbii	$$⊢\left[x/z\right]\left[y/x\right]\left[z/y\right]x=y\leftrightarrow \left[x/z\right]\left[y/x\right]x=z$$
3		equsb3	$$⊢\left[y/x\right]x=z\leftrightarrow y=z$$
4	3	sbbii	$$⊢\left[x/z\right]\left[y/x\right]x=z\leftrightarrow \left[x/z\right]y=z$$
5		equsb3r	$$⊢\left[x/z\right]y=z\leftrightarrow y=x$$
6		equcom	$$⊢y=x\leftrightarrow x=y$$
7	5 6	bitri	$$⊢\left[x/z\right]y=z\leftrightarrow x=y$$
8	2 4 7	3bitri	$$⊢\left[x/z\right]\left[y/x\right]\left[z/y\right]x=y\leftrightarrow x=y$$
9	8	gen2	$$⊢\forall x\forall y\left(\left[x/z\right]\left[y/x\right]\left[z/y\right]x=y\leftrightarrow x=y\right)$$
10		df-ich	$$⊢\left[x\rightleftarrows y\right]x=y\leftrightarrow \forall x\forall y\left(\left[x/z\right]\left[y/x\right]\left[z/y\right]x=y\leftrightarrow x=y\right)$$
11	9 10	mpbir	$$⊢\left[x\rightleftarrows y\right]x=y$$