Metamath Proof Explorer


Theorem nfich1

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

Ref Expression
Assertion nfich1 x x y φ

Proof

Step Hyp Ref Expression
1 df-ich x y φ x y x a y x a y φ φ
2 nfa1 x x y x a y x a y φ φ
3 1 2 nfxfr x x y φ