Theorem nfcvd 2373

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

Syntax hints:   → wi 4  Ⅎwnfc 2359

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 1495  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-nfc 2361

This theorem is referenced by:  nfeld  2388  nfraldw  2562  vtoclgft  2852  vtocld  2854  sbcralt  3106  sbcrext  3107  csbied  3172  csbie2t  3174  sbcco3g  3183  csbco3g  3184  dfnfc2  3909  eusvnfb  4549  eusv2i  4550  peano2  4691  iota2d  5311  iota2  5314  fmptcof  5810  riotaeqimp  5991  riota5f  5993  riota5  5994  fmpoco  6376  nfixpxy  6881  nfnegd  8368  iseqf1olemjpcl  10763  iseqf1olemqpcl  10764  iseqf1olemfvp  10765  seq3f1olemqsum  10768  fprodeq0g  12192  pcmpt  12909  strcollnft  16529