Theorem nfcvd 2348

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

Syntax hints:   -> wi 4   F/_wnfc 2334

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 1471  ax-17 1548

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-nfc 2336

This theorem is referenced by:  nfeld  2363  nfraldw  2537  vtoclgft  2822  vtocld  2824  sbcralt  3074  sbcrext  3075  csbied  3139  csbie2t  3141  sbcco3g  3150  csbco3g  3151  dfnfc2  3867  eusvnfb  4500  eusv2i  4501  peano2  4642  iota2d  5257  iota2  5260  fmptcof  5746  riota5f  5923  riota5  5924  fmpoco  6301  nfixpxy  6803  nfnegd  8267  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  iseqf1olemfvp  10653  seq3f1olemqsum  10656  fprodeq0g  11891  pcmpt  12608  strcollnft  15853