Theorem nfcvd 2375

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

Syntax hints:   → wi 4  Ⅎwnfc 2361

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 1497  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-nfc 2363

This theorem is referenced by:  nfeld  2390  nfraldw  2564  vtoclgft  2854  vtocld  2856  sbcralt  3108  sbcrext  3109  csbied  3174  csbie2t  3176  sbcco3g  3185  csbco3g  3186  dfnfc2  3911  eusvnfb  4551  eusv2i  4552  peano2  4693  iota2d  5313  iota2  5316  fmptcof  5814  riotaeqimp  5996  riota5f  5998  riota5  5999  fmpoco  6381  nfixpxy  6886  nfnegd  8375  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsum  10776  fprodeq0g  12201  pcmpt  12918  strcollnft  16600