Theorem nfcvd 2220

Description: If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfcvd	|- ( ph -> F/_ x A )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem nfcvd

Step	Hyp	Ref	Expression
1		nfcv 2219	. 2 |- F/_ x A
2	1	a1i 9	1 |- ( ph -> F/_ x A )

Syntax hints:   -> wi 4   F/_wnfc 2206

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-nfc 2208

This theorem is referenced by:  nfeld  2234  vtoclgft  2649  vtocld  2651  sbcralt  2890  sbcrext  2891  csbied  2948  csbie2t  2950  sbcco3g  2959  csbco3g  2960  dfnfc2  3619  eusvnfb  4204  eusv2i  4205  peano2  4336  iota2d  4912  iota2  4913  fmptcof  5352  riota5f  5512  riota5  5513  fmpt2co  5857  nfnegd  7304  strcollnft  10779