ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfcvd GIF version

Theorem nfcvd 2282
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
StepHypRef Expression
1 nfcv 2281 . 2 𝑥𝐴
21a1i 9 1 (𝜑𝑥𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wnfc 2268
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 1425  ax-17 1506
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-nfc 2270
This theorem is referenced by:  nfeld  2297  vtoclgft  2736  vtocld  2738  sbcralt  2985  sbcrext  2986  csbied  3046  csbie2t  3048  sbcco3g  3057  csbco3g  3058  dfnfc2  3754  eusvnfb  4375  eusv2i  4376  peano2  4509  iota2d  5113  iota2  5114  fmptcof  5587  riota5f  5754  riota5  5755  fmpoco  6113  nfixpxy  6611  nfnegd  7970  iseqf1olemjpcl  10280  iseqf1olemqpcl  10281  iseqf1olemfvp  10282  seq3f1olemqsum  10285  strcollnft  13241
  Copyright terms: Public domain W3C validator