Theorem nfich2

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

	Ref	Expression
Assertion	nfich2	$$⊢Ⅎy\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		nfa2	$$⊢Ⅎy\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	$$⊢Ⅎy\left[x\rightleftarrows y\right]\phi$$