This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfich2

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

		Ref	Expression
	Assertion	nfich2	$⊢ Ⅎ y [x ⇄ y] φ$

Step	Hyp	Ref	Expression
1		df-ich	$⊢ [x ⇄ y] φ \leftrightarrow \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
2		nfa2	$⊢ Ⅎ y \forall x \forall y ([x/ a] [y/ x] [a/ y] φ \leftrightarrow φ)$
3	1 2	nfxfr	$⊢ Ⅎ y [x ⇄ y] φ$