Metamath Proof Explorer
Description: If x is disjoint from A , then x is not free in A .
(Contributed by Mario Carneiro, 7Oct2016)


Ref 
Expression 

Assertion 
nfcvd 
$${\u22a2}{\phi}\to \underset{\_}{\u2132}{x}\phantom{\rule{.4em}{0ex}}{A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nfcv 
$${\u22a2}\underset{\_}{\u2132}{x}\phantom{\rule{.4em}{0ex}}{A}$$ 
2 
1

a1i 
$${\u22a2}{\phi}\to \underset{\_}{\u2132}{x}\phantom{\rule{.4em}{0ex}}{A}$$ 