Theorem nfcvd 2374

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

Syntax hints:   → wi 4  Ⅎwnfc 2360

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 2362

This theorem is referenced by:  nfeld  2389  nfraldw  2563  vtoclgft  2853  vtocld  2855  sbcralt  3107  sbcrext  3108  csbied  3173  csbie2t  3175  sbcco3g  3184  csbco3g  3185  dfnfc2  3912  eusvnfb  4553  eusv2i  4554  peano2  4695  iota2d  5315  iota2  5318  fmptcof  5817  riotaeqimp  6001  riota5f  6003  riota5  6004  fmpoco  6386  nfixpxy  6891  nfnegd  8380  iseqf1olemjpcl  10776  iseqf1olemqpcl  10777  iseqf1olemfvp  10778  seq3f1olemqsum  10781  fprodeq0g  12222  pcmpt  12939  strcollnft  16639