Metamath Proof Explorer

Theorem nfich1

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

Ref Expression
Assertion nfich1 
|- F/ x [ x <> y ] ph

Proof

Step Hyp Ref Expression
1 df-ich 
 |-  ( [ x <> y ] ph <-> A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) )
2 nfa1 
 |-  F/ x A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph )
3 1 2 nfxfr 
 |-  F/ x [ x <> y ] ph