Theorem nfcvd 2387

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

Syntax hints:   -> wi 4   F/_wnfc 2373

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 2375

This theorem is referenced by:  nfeld  2402  nfraldw  2576  vtoclgft  2867  vtocld  2869  sbcralt  3122  sbcrext  3123  csbied  3188  csbie2t  3190  sbcco3g  3199  csbco3g  3200  ifeqeqxdc  3673  dfnfc2  3937  eusvnfb  4580  eusv2i  4581  peano2  4722  iota2d  5344  iota2  5347  fmptcof  5849  riotaeqimp  6036  riota5f  6038  riota5  6039  fmpoco  6425  nfixpxy  6965  nfnegd  8485  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsum  10899  fprodeq0g  12349  pcmpt  13066  strcollnft  16880