Theorem nfcvd 2280

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

Syntax hints:   -> wi 4   F/_wnfc 2266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-nfc 2268

This theorem is referenced by:  nfeld  2295  vtoclgft  2731  vtocld  2733  sbcralt  2980  sbcrext  2981  csbied  3041  csbie2t  3043  sbcco3g  3052  csbco3g  3053  dfnfc2  3749  eusvnfb  4370  eusv2i  4371  peano2  4504  iota2d  5108  iota2  5109  fmptcof  5580  riota5f  5747  riota5  5748  fmpoco  6106  nfixpxy  6604  nfnegd  7951  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  iseqf1olemfvp  10263  seq3f1olemqsum  10266  strcollnft  13171