Metamath Proof Explorer

Theorem nfcii

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

Ref Expression
Hypothesis nfcii.1 
|- ( y e. A -> A. x y e. A )
Assertion nfcii 
|- F/_ x A

Proof

Step Hyp Ref Expression
1 nfcii.1 
 |-  ( y e. A -> A. x y e. A )
2 1 nf5i 
 |-  F/ x y e. A
3 2 nfci 
 |-  F/_ x A