Theorem ichid

Description: A setvar variable is always interchangeable with itself. (Contributed by AV, 29-Jul-2023)

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

Proof

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