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

Theorem nfcvd 2229
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 2228 . 2 𝑥𝐴
21a1i 9 1 (𝜑𝑥𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wnfc 2215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383  ax-17 1464
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-nfc 2217
This theorem is referenced by:  nfeld  2244  vtoclgft  2669  vtocld  2671  sbcralt  2913  sbcrext  2914  csbied  2972  csbie2t  2974  sbcco3g  2983  csbco3g  2984  dfnfc2  3666  eusvnfb  4267  eusv2i  4268  peano2  4400  iota2d  4992  iota2  4993  fmptcof  5449  riota5f  5614  riota5  5615  fmpt2co  5963  nfnegd  7657  iseqf1olemjpcl  9889  iseqf1olemqpcl  9890  iseqf1olemfvp  9891  seq3f1olemqsum  9894  strcollnft  11525
  Copyright terms: Public domain W3C validator