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

Theorem nfcvd 2157
Description: If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfcvd (φxA)
Distinct variable group:   x,A
Allowed substitution hint:   φ(x)

Proof of Theorem nfcvd
StepHypRef Expression
1 nfcv 2156 . 2 xA
21a1i 9 1 (φxA)
Colors of variables: wff set class
Syntax hints:  wi 4  wnfc 2143
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1314  ax-17 1396
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-nfc 2145
This theorem is referenced by:  nfeld  2171  vtoclgft  2577  vtocld  2579  sbcralt  2807  sbcrext  2808  csbied  2865  csbie2t  2867  sbcco3g  2876  csbco3g  2877  dfnfc2  3568  eusvnfb  4132  eusv2i  4133  peano2  4241  iota2d  4815  iota2  4816  fmptcof  5252  riota5f  5412  riota5  5413  fmpt2co  5756  nfnegd  6794  strcollnft  7341
  Copyright terms: Public domain W3C validator