Theorem nfcvd 2350

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

Syntax hints:   → wi 4  Ⅎwnfc 2336

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 1473  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-nfc 2338

This theorem is referenced by:  nfeld  2365  nfraldw  2539  vtoclgft  2824  vtocld  2826  sbcralt  3076  sbcrext  3077  csbied  3141  csbie2t  3143  sbcco3g  3152  csbco3g  3153  dfnfc2  3870  eusvnfb  4505  eusv2i  4506  peano2  4647  iota2d  5263  iota2  5266  fmptcof  5754  riota5f  5931  riota5  5932  fmpoco  6309  nfixpxy  6811  nfnegd  8275  iseqf1olemjpcl  10660  iseqf1olemqpcl  10661  iseqf1olemfvp  10662  seq3f1olemqsum  10665  fprodeq0g  11993  pcmpt  12710  strcollnft  15994