Theorem nfcvd 2376

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

Syntax hints:   -> wi 4   F/_wnfc 2362

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 2364

This theorem is referenced by:  nfeld  2391  nfraldw  2565  vtoclgft  2855  vtocld  2857  sbcralt  3109  sbcrext  3110  csbied  3175  csbie2t  3177  sbcco3g  3186  csbco3g  3187  dfnfc2  3916  eusvnfb  4557  eusv2i  4558  peano2  4699  iota2d  5320  iota2  5323  fmptcof  5822  riotaeqimp  6006  riota5f  6008  riota5  6009  fmpoco  6390  nfixpxy  6929  nfnegd  8417  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  iseqf1olemfvp  10818  seq3f1olemqsum  10821  fprodeq0g  12262  pcmpt  12979  strcollnft  16683