Theorem ichv

Description: Setvar variables are interchangeable in a wff they do not appear in. (Contributed by SN, 23-Nov-2023)

	Ref	Expression
Assertion	ichv	$$⊢\left[x\rightleftarrows y\right]\phi$$

Proof

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