Theorem nfcvd 2320

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

Syntax hints:   -> wi 4   F/_wnfc 2306

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 1449  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-nfc 2308

This theorem is referenced by:  nfeld  2335  nfraldw  2509  vtoclgft  2789  vtocld  2791  sbcralt  3041  sbcrext  3042  csbied  3105  csbie2t  3107  sbcco3g  3116  csbco3g  3117  dfnfc2  3829  eusvnfb  4456  eusv2i  4457  peano2  4596  iota2d  5205  iota2  5208  fmptcof  5685  riota5f  5857  riota5  5858  fmpoco  6219  nfixpxy  6719  nfnegd  8155  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  iseqf1olemfvp  10499  seq3f1olemqsum  10502  fprodeq0g  11648  pcmpt  12343  strcollnft  14775