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

Theorem nfcvd 2333
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  |-  ( ph  -> 
F/_ x A )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem nfcvd
StepHypRef Expression
1 nfcv 2332 . 2  |-  F/_ x A
21a1i 9 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2319
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 1460  ax-17 1537
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-nfc 2321
This theorem is referenced by:  nfeld  2348  nfraldw  2522  vtoclgft  2802  vtocld  2804  sbcralt  3054  sbcrext  3055  csbied  3118  csbie2t  3120  sbcco3g  3129  csbco3g  3130  dfnfc2  3842  eusvnfb  4469  eusv2i  4470  peano2  4609  iota2d  5218  iota2  5221  fmptcof  5699  riota5f  5871  riota5  5872  fmpoco  6235  nfixpxy  6735  nfnegd  8171  iseqf1olemjpcl  10513  iseqf1olemqpcl  10514  iseqf1olemfvp  10515  seq3f1olemqsum  10518  fprodeq0g  11664  pcmpt  12359  strcollnft  15133
  Copyright terms: Public domain W3C validator