Metamath Proof Explorer

Theorem nfcd

Description: Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypotheses nfcd.1 y φ
nfcd.2 φ x y A
Assertion nfcd φ _ x A


Step Hyp Ref Expression
1 nfcd.1 y φ
2 nfcd.2 φ x y A
3 1 2 alrimi φ y x y A
4 df-nfc _ x A y x y A
5 3 4 sylibr φ _ x A