Theorem nfcvd 2282

Description: If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfcvd	⊢ (𝜑 → Ⅎ𝑥𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfcvd

Step	Hyp	Ref	Expression
1		nfcv 2281	. 2 ⊢ Ⅎ𝑥𝐴
2	1	a1i 9	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4  Ⅎwnfc 2268

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

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-nfc 2270

This theorem is referenced by:  nfeld  2297  vtoclgft  2736  vtocld  2738  sbcralt  2985  sbcrext  2986  csbied  3046  csbie2t  3048  sbcco3g  3057  csbco3g  3058  dfnfc2  3754  eusvnfb  4375  eusv2i  4376  peano2  4509  iota2d  5113  iota2  5114  fmptcof  5587  riota5f  5754  riota5  5755  fmpoco  6113  nfixpxy  6611  nfnegd  7958  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  iseqf1olemfvp  10270  seq3f1olemqsum  10273  strcollnft  13182