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  3121  sbcrext  3122  csbied  3187  csbie2t  3189  sbcco3g  3198  csbco3g  3199  dfnfc2  3934  eusvnfb  4577  eusv2i  4578  peano2  4719  iota2d  5341  iota2  5344  fmptcof  5846  riotaeqimp  6030  riota5f  6032  riota5  6033  fmpoco  6414  nfixpxy  6954  nfnegd  8474  iseqf1olemjpcl  10877  iseqf1olemqpcl  10878  iseqf1olemfvp  10879  seq3f1olemqsum  10882  fprodeq0g  12332  pcmpt  13049  strcollnft  16803