Theorem nfcvd 2393

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

Syntax hints:   → wi 4  Ⅎwnfc 2379

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 1502  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-nfc 2381

This theorem is referenced by:  nfeld  2408  nfraldw  2582  vtoclgft  2873  vtocld  2875  sbcralt  3128  sbcrext  3129  csbied  3194  csbie2t  3196  sbcco3g  3205  csbco3g  3206  ifeqeqxdc  3687  dfnfc2  3951  eusvnfb  4598  eusv2i  4599  peano2  4740  iota2d  5362  iota2  5365  fmptcof  5869  riotaeqimp  6057  riota5f  6059  riota5  6060  fmpoco  6446  nfixpxy  6993  nfnegd  8516  iseqf1olemjpcl  10928  iseqf1olemqpcl  10929  iseqf1olemfvp  10930  seq3f1olemqsum  10933  fprodeq0g  12388  pcmpt  13105  strcollnft  16993