Theorem nfcvd 2393

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

This proof depends on syntax axioms:   -> wi 4   F/_wnfc 2379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-nfc 2381

This theorem is used by:  nfeld  2408  nfraldw  2582  vtoclgft  2873  vtocld  2875  sbcralt  3128  sbcrext  3129  csbied  3194  csbie2t  3196  sbcco3g  3205  csbco3g  3206  ifeqeqxdc  3687  dfnfc2  3953  eusvnfb  4600  eusv2i  4601  peano2  4742  iota2d  5364  iota2  5367  fmptcof  5875  riotaeqimp  6063  riota5f  6065  riota5  6066  fmpoco  6452  nfixpxy  6999  nfnegd  8524  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsum  10965  fprodeq0g  12424  pcmpt  13145  strcollnft  17176