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

Theorem nfcvd 2259
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 2258 . 2  |-  F/_ x A
21a1i 9 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1410  ax-17 1491
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-nfc 2247
This theorem is referenced by:  nfeld  2274  vtoclgft  2710  vtocld  2712  sbcralt  2957  sbcrext  2958  csbied  3016  csbie2t  3018  sbcco3g  3027  csbco3g  3028  dfnfc2  3724  eusvnfb  4345  eusv2i  4346  peano2  4479  iota2d  5083  iota2  5084  fmptcof  5555  riota5f  5722  riota5  5723  fmpoco  6081  nfixpxy  6579  nfnegd  7926  iseqf1olemjpcl  10236  iseqf1olemqpcl  10237  iseqf1olemfvp  10238  seq3f1olemqsum  10241  strcollnft  13109
  Copyright terms: Public domain W3C validator