Theorem nfich1

Description: The first interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		nfa1	$$⊢Ⅎx\forall x\forall y\left(\left[x/a\right]\left[y/x\right]\left[a/y\right]\phi \leftrightarrow \phi \right)$$
3	1 2	nfxfr	$$⊢Ⅎx\left[x\rightleftarrows y\right]\phi$$