Theorem nfcvd 2375

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

Syntax hints:   -> wi 4   F/_wnfc 2361

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 1497  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-nfc 2363

This theorem is referenced by:  nfeld  2390  nfraldw  2564  vtoclgft  2854  vtocld  2856  sbcralt  3108  sbcrext  3109  csbied  3174  csbie2t  3176  sbcco3g  3185  csbco3g  3186  dfnfc2  3911  eusvnfb  4551  eusv2i  4552  peano2  4693  iota2d  5313  iota2  5316  fmptcof  5814  riotaeqimp  5995  riota5f  5997  riota5  5998  fmpoco  6380  nfixpxy  6885  nfnegd  8374  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsum  10774  fprodeq0g  12198  pcmpt  12915  strcollnft  16579