Description: The second interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | nfich2 | |- F/ y [ x <> y ] ph |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ich | |- ( [ x <> y ] ph <-> A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) ) |
|
2 | nfa2 | |- F/ y A. x A. y ( [ x / a ] [ y / x ] [ a / y ] ph <-> ph ) |
|
3 | 1 2 | nfxfr | |- F/ y [ x <> y ] ph |