Theorem nfcvd 2353

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

Syntax hints:   → wi 4  Ⅎwnfc 2339

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 1475  ax-17 1552

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-nfc 2341

This theorem is referenced by:  nfeld  2368  nfraldw  2542  vtoclgft  2831  vtocld  2833  sbcralt  3085  sbcrext  3086  csbied  3151  csbie2t  3153  sbcco3g  3162  csbco3g  3163  dfnfc2  3885  eusvnfb  4522  eusv2i  4523  peano2  4664  iota2d  5281  iota2  5284  fmptcof  5775  riotaeqimp  5952  riota5f  5954  riota5  5955  fmpoco  6332  nfixpxy  6834  nfnegd  8310  iseqf1olemjpcl  10697  iseqf1olemqpcl  10698  iseqf1olemfvp  10699  seq3f1olemqsum  10702  fprodeq0g  12115  pcmpt  12832  strcollnft  16257