Theorem nfcvd 2313

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

Syntax hints:   → wi 4  Ⅎwnfc 2299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-nfc 2301

This theorem is referenced by:  nfeld  2328  nfraldw  2502  vtoclgft  2780  vtocld  2782  sbcralt  3031  sbcrext  3032  csbied  3095  csbie2t  3097  sbcco3g  3106  csbco3g  3107  dfnfc2  3812  eusvnfb  4437  eusv2i  4438  peano2  4577  iota2d  5183  iota2  5186  fmptcof  5660  riota5f  5830  riota5  5831  fmpoco  6192  nfixpxy  6691  nfnegd  8102  iseqf1olemjpcl  10438  iseqf1olemqpcl  10439  iseqf1olemfvp  10440  seq3f1olemqsum  10443  fprodeq0g  11588  pcmpt  12282  strcollnft  13941