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  2788  vtocld  2790  sbcralt  3040  sbcrext  3041  csbied  3104  csbie2t  3106  sbcco3g  3115  csbco3g  3116  dfnfc2  3828  eusvnfb  4455  eusv2i  4456  peano2  4595  iota2d  5204  iota2  5207  fmptcof  5684  riota5f  5855  riota5  5856  fmpoco  6217  nfixpxy  6717  nfnegd  8153  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  iseqf1olemfvp  10497  seq3f1olemqsum  10500  fprodeq0g  11646  pcmpt  12341  strcollnft  14739