Theorem nfcvd 2309

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

Syntax hints:   -> wi 4   F/_wnfc 2295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-nfc 2297

This theorem is referenced by:  nfeld  2324  nfraldw  2498  vtoclgft  2776  vtocld  2778  sbcralt  3027  sbcrext  3028  csbied  3091  csbie2t  3093  sbcco3g  3102  csbco3g  3103  dfnfc2  3807  eusvnfb  4432  eusv2i  4433  peano2  4572  iota2d  5178  iota2  5179  fmptcof  5652  riota5f  5822  riota5  5823  fmpoco  6184  nfixpxy  6683  nfnegd  8094  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  iseqf1olemfvp  10432  seq3f1olemqsum  10435  fprodeq0g  11579  pcmpt  12273  strcollnft  13866