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  2810  vtocld  2812  sbcralt  3062  sbcrext  3063  csbied  3127  csbie2t  3129  sbcco3g  3138  csbco3g  3139  dfnfc2  3853  eusvnfb  4485  eusv2i  4486  peano2  4627  iota2d  5241  iota2  5244  fmptcof  5725  riota5f  5898  riota5  5899  fmpoco  6269  nfixpxy  6771  nfnegd  8215  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsum  10584  fprodeq0g  11781  pcmpt  12481  strcollnft  15476