Theorem nfcvd 2337

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

Syntax hints:   -> wi 4   F/_wnfc 2323

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 1460  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-nfc 2325

This theorem is referenced by:  nfeld  2352  nfraldw  2526  vtoclgft  2811  vtocld  2813  sbcralt  3063  sbcrext  3064  csbied  3128  csbie2t  3130  sbcco3g  3139  csbco3g  3140  dfnfc2  3854  eusvnfb  4486  eusv2i  4487  peano2  4628  iota2d  5242  iota2  5245  fmptcof  5726  riota5f  5899  riota5  5900  fmpoco  6271  nfixpxy  6773  nfnegd  8217  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsum  10587  fprodeq0g  11784  pcmpt  12484  strcollnft  15546