Theorem nfcvd 2350

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

Syntax hints:   -> wi 4   F/_wnfc 2336

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 1473  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-nfc 2338

This theorem is referenced by:  nfeld  2365  nfraldw  2539  vtoclgft  2825  vtocld  2827  sbcralt  3079  sbcrext  3080  csbied  3144  csbie2t  3146  sbcco3g  3155  csbco3g  3156  dfnfc2  3877  eusvnfb  4514  eusv2i  4515  peano2  4656  iota2d  5272  iota2  5275  fmptcof  5765  riota5f  5942  riota5  5943  fmpoco  6320  nfixpxy  6822  nfnegd  8298  iseqf1olemjpcl  10685  iseqf1olemqpcl  10686  iseqf1olemfvp  10687  seq3f1olemqsum  10690  fprodeq0g  12034  pcmpt  12751  strcollnft  16089