Theorem nfcvd 2340

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

Syntax hints:   -> wi 4   F/_wnfc 2326

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 1463  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-nfc 2328

This theorem is referenced by:  nfeld  2355  nfraldw  2529  vtoclgft  2814  vtocld  2816  sbcralt  3066  sbcrext  3067  csbied  3131  csbie2t  3133  sbcco3g  3142  csbco3g  3143  dfnfc2  3857  eusvnfb  4489  eusv2i  4490  peano2  4631  iota2d  5245  iota2  5248  fmptcof  5729  riota5f  5902  riota5  5903  fmpoco  6274  nfixpxy  6776  nfnegd  8222  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsum  10605  fprodeq0g  11803  pcmpt  12512  strcollnft  15630