Theorem nfcvd 2387

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

Syntax hints:   → wi 4  Ⅎwnfc 2373

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 2375

This theorem is referenced by:  nfeld  2402  nfraldw  2576  vtoclgft  2867  vtocld  2869  sbcralt  3122  sbcrext  3123  csbied  3188  csbie2t  3190  sbcco3g  3199  csbco3g  3200  ifeqeqxdc  3673  dfnfc2  3937  eusvnfb  4580  eusv2i  4581  peano2  4722  iota2d  5344  iota2  5347  fmptcof  5849  riotaeqimp  6036  riota5f  6038  riota5  6039  fmpoco  6425  nfixpxy  6965  nfnegd  8486  iseqf1olemjpcl  10897  iseqf1olemqpcl  10898  iseqf1olemfvp  10899  seq3f1olemqsum  10902  fprodeq0g  12352  pcmpt  13069  strcollnft  16893