Theorem ichf

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

	Ref	Expression
Hypotheses	ichf.1	$$⊢Ⅎx\phi$$
	ichf.2	$$⊢Ⅎy\phi$$
Assertion	ichf	$$⊢\left[x\rightleftarrows y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		ichf.1	$$⊢Ⅎx\phi$$
2		ichf.2	$$⊢Ⅎy\phi$$
3	2	sbf	$$⊢\left[a/y\right]\phi \leftrightarrow \phi$$
4	3	sbbii	$$⊢\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \left[y/x\right]\phi$$
5	1	sbf	$$⊢\left[y/x\right]\phi \leftrightarrow \phi$$
6	4 5	bitri	$$⊢\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi$$
7	6	sbbii	$$⊢\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \left[x/a\right]\phi$$
8		sbv	$$⊢\left[x/a\right]\phi \leftrightarrow \phi$$
9	7 8	bitri	$$⊢\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi$$
10	9	gen2	$$⊢\forall x\forall y\left(\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi \right)$$
11		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)$$
12	10 11	mpbir	$$⊢\left[x\rightleftarrows y\right]\phi$$