Theorem nfcvd 2241

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

Syntax hints:   -> wi 4   F/_wnfc 2227

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-17 1474

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-nfc 2229

This theorem is referenced by:  nfeld  2256  vtoclgft  2691  vtocld  2693  sbcralt  2937  sbcrext  2938  csbied  2996  csbie2t  2998  sbcco3g  3007  csbco3g  3008  dfnfc2  3701  eusvnfb  4313  eusv2i  4314  peano2  4447  iota2d  5049  iota2  5050  fmptcof  5519  riota5f  5686  riota5  5687  fmpoco  6043  nfixpxy  6541  nfnegd  7829  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  iseqf1olemfvp  10111  seq3f1olemqsum  10114  strcollnft  12767