Theorem nfcvd 2349

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

Syntax hints:   -> wi 4   F/_wnfc 2335

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 1472  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-nfc 2337

This theorem is referenced by:  nfeld  2364  nfraldw  2538  vtoclgft  2823  vtocld  2825  sbcralt  3075  sbcrext  3076  csbied  3140  csbie2t  3142  sbcco3g  3151  csbco3g  3152  dfnfc2  3868  eusvnfb  4501  eusv2i  4502  peano2  4643  iota2d  5258  iota2  5261  fmptcof  5747  riota5f  5924  riota5  5925  fmpoco  6302  nfixpxy  6804  nfnegd  8268  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsum  10658  fprodeq0g  11949  pcmpt  12666  strcollnft  15920