Theorem nfcvd 2320

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

Syntax hints:   → wi 4  Ⅎwnfc 2306

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 1449  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-nfc 2308

This theorem is referenced by:  nfeld  2335  nfraldw  2509  vtoclgft  2787  vtocld  2789  sbcralt  3039  sbcrext  3040  csbied  3103  csbie2t  3105  sbcco3g  3114  csbco3g  3115  dfnfc2  3827  eusvnfb  4454  eusv2i  4455  peano2  4594  iota2d  5203  iota2  5206  fmptcof  5683  riota5f  5854  riota5  5855  fmpoco  6216  nfixpxy  6716  nfnegd  8152  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  iseqf1olemfvp  10496  seq3f1olemqsum  10499  fprodeq0g  11645  pcmpt  12340  strcollnft  14706