Theorem nfcvd 2385

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

Syntax hints:   -> wi 4   F/_wnfc 2371

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 1498  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-nfc 2373

This theorem is referenced by:  nfeld  2400  nfraldw  2574  vtoclgft  2865  vtocld  2867  sbcralt  3119  sbcrext  3120  csbied  3185  csbie2t  3187  sbcco3g  3196  csbco3g  3197  dfnfc2  3932  eusvnfb  4575  eusv2i  4576  peano2  4717  iota2d  5339  iota2  5342  fmptcof  5844  riotaeqimp  6028  riota5f  6030  riota5  6031  fmpoco  6412  nfixpxy  6952  nfnegd  8469  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsum  10875  fprodeq0g  12324  pcmpt  13041  strcollnft  16754