Theorem nfcvd 2320

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

Syntax hints:   → wi 4  Ⅎwnfc 2306

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 1449  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-nfc 2308

This theorem is referenced by:  nfeld  2335  nfraldw  2509  vtoclgft  2787  vtocld  2789  sbcralt  3039  sbcrext  3040  csbied  3103  csbie2t  3105  sbcco3g  3114  csbco3g  3115  dfnfc2  3826  eusvnfb  4452  eusv2i  4453  peano2  4592  iota2d  5200  iota2  5203  fmptcof  5680  riota5f  5850  riota5  5851  fmpoco  6212  nfixpxy  6712  nfnegd  8147  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  iseqf1olemfvp  10490  seq3f1olemqsum  10493  fprodeq0g  11637  pcmpt  12331  strcollnft  14507