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

Theorem nfcvd 2176
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 2175 . 2 xA
21a1i 9 1 (φxA)
Colors of variables: wff set class
Syntax hints:  wi 4  wnfc 2162
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 1335  ax-17 1416
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-nfc 2164
This theorem is referenced by:  nfeld  2190  vtoclgft  2598  vtocld  2600  sbcralt  2828  sbcrext  2829  csbied  2886  csbie2t  2888  sbcco3g  2897  csbco3g  2898  dfnfc2  3589  eusvnfb  4152  eusv2i  4153  peano2  4261  iota2d  4835  iota2  4836  fmptcof  5274  riota5f  5435  riota5  5436  fmpt2co  5779  nfnegd  6964  strcollnft  9368
  Copyright terms: Public domain W3C validator