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 )

Syntax hints:   -> wi 4   F/_wnfc 2379

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 1502  ax-17 1579

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

This theorem is referenced by:  nfeld  2408  nfraldw  2582  vtoclgft  2873  vtocld  2875  sbcralt  3128  sbcrext  3129  csbied  3194  csbie2t  3196  sbcco3g  3205  csbco3g  3206  ifeqeqxdc  3684  dfnfc2  3948  eusvnfb  4595  eusv2i  4596  peano2  4737  iota2d  5359  iota2  5362  fmptcof  5866  riotaeqimp  6053  riota5f  6055  riota5  6056  fmpoco  6442  nfixpxy  6989  nfnegd  8512  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsum  10928  fprodeq0g  12383  pcmpt  13100  strcollnft  16924