Theorem nfcvd 2385

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

Syntax hints:   → wi 4  Ⅎwnfc 2371

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 1498  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-nfc 2373

This theorem is referenced by:  nfeld  2400  nfraldw  2574  vtoclgft  2864  vtocld  2866  sbcralt  3118  sbcrext  3119  csbied  3184  csbie2t  3186  sbcco3g  3195  csbco3g  3196  dfnfc2  3931  eusvnfb  4574  eusv2i  4575  peano2  4716  iota2d  5338  iota2  5341  fmptcof  5843  riotaeqimp  6027  riota5f  6029  riota5  6030  fmpoco  6411  nfixpxy  6951  nfnegd  8465  iseqf1olemjpcl  10866  iseqf1olemqpcl  10867  iseqf1olemfvp  10868  seq3f1olemqsum  10871  fprodeq0g  12317  pcmpt  13034  strcollnft  16741