Metamath Proof Explorer


Theorem nfich1

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

Ref Expression
Assertion nfich1 𝑥 [ 𝑥𝑦 ] 𝜑

Proof

Step Hyp Ref Expression
1 df-ich ( [ 𝑥𝑦 ] 𝜑 ↔ ∀ 𝑥𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑𝜑 ) )
2 nfa1 𝑥𝑥𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑𝜑 )
3 1 2 nfxfr 𝑥 [ 𝑥𝑦 ] 𝜑