Theorem nfcvd 2333

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 2332	. 2 |- F/_ x A
2	1	a1i 9	1 |- ( ph -> F/_ x A )

Syntax hints:   -> wi 4   F/_wnfc 2319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-nfc 2321

This theorem is referenced by:  nfeld  2348  nfraldw  2522  vtoclgft  2802  vtocld  2804  sbcralt  3054  sbcrext  3055  csbied  3118  csbie2t  3120  sbcco3g  3129  csbco3g  3130  dfnfc2  3842  eusvnfb  4469  eusv2i  4470  peano2  4609  iota2d  5218  iota2  5221  fmptcof  5699  riota5f  5871  riota5  5872  fmpoco  6235  nfixpxy  6735  nfnegd  8171  iseqf1olemjpcl  10513  iseqf1olemqpcl  10514  iseqf1olemfvp  10515  seq3f1olemqsum  10518  fprodeq0g  11664  pcmpt  12359  strcollnft  15133