Metamath Proof Explorer

Theorem nfcrd

Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016)

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

Proof

Step Hyp Ref Expression
1 nfcrd.1 
 |-  ( ph -> F/_ x A )
2 nfcr 
 |-  ( F/_ x A -> F/ x y e. A )
3 1 2 syl 
 |-  ( ph -> F/ x y e. A )