Theorem nfcvd 2283

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

Syntax hints:   → wi 4  Ⅎwnfc 2269

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 1426  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-nfc 2271

This theorem is referenced by:  nfeld  2298  vtoclgft  2739  vtocld  2741  sbcralt  2989  sbcrext  2990  csbied  3051  csbie2t  3053  sbcco3g  3062  csbco3g  3063  dfnfc2  3762  eusvnfb  4383  eusv2i  4384  peano2  4517  iota2d  5121  iota2  5122  fmptcof  5595  riota5f  5762  riota5  5763  fmpoco  6121  nfixpxy  6619  nfnegd  7982  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsum  10304  strcollnft  13353