Theorem nfcvd 2373

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 2372	. 2 ⊢ Ⅎ𝑥𝐴
2	1	a1i 9	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4  Ⅎwnfc 2359

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 1495  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-nfc 2361

This theorem is referenced by:  nfeld  2388  nfraldw  2562  vtoclgft  2851  vtocld  2853  sbcralt  3105  sbcrext  3106  csbied  3171  csbie2t  3173  sbcco3g  3182  csbco3g  3183  dfnfc2  3906  eusvnfb  4545  eusv2i  4546  peano2  4687  iota2d  5305  iota2  5308  fmptcof  5804  riotaeqimp  5985  riota5f  5987  riota5  5988  fmpoco  6368  nfixpxy  6872  nfnegd  8350  iseqf1olemjpcl  10738  iseqf1olemqpcl  10739  iseqf1olemfvp  10740  seq3f1olemqsum  10743  fprodeq0g  12157  pcmpt  12874  strcollnft  16371