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

Theorem nfcvd 2330
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 2329 . 2 𝑥𝐴
21a1i 9 1 (𝜑𝑥𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wnfc 2316
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 1459  ax-17 1536
This theorem depends on definitions:  df-bi 117  df-nf 1471  df-nfc 2318
This theorem is referenced by:  nfeld  2345  nfraldw  2519  vtoclgft  2799  vtocld  2801  sbcralt  3051  sbcrext  3052  csbied  3115  csbie2t  3117  sbcco3g  3126  csbco3g  3127  dfnfc2  3839  eusvnfb  4466  eusv2i  4467  peano2  4606  iota2d  5215  iota2  5218  fmptcof  5696  riota5f  5868  riota5  5869  fmpoco  6231  nfixpxy  6731  nfnegd  8167  iseqf1olemjpcl  10509  iseqf1olemqpcl  10510  iseqf1olemfvp  10511  seq3f1olemqsum  10514  fprodeq0g  11660  pcmpt  12355  strcollnft  15032
  Copyright terms: Public domain W3C validator