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

Theorem nfcvd 2313
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 2312 . 2  |-  F/_ x A
21a1i 9 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2299
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 1442  ax-17 1519
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-nfc 2301
This theorem is referenced by:  nfeld  2328  nfraldw  2502  vtoclgft  2780  vtocld  2782  sbcralt  3031  sbcrext  3032  csbied  3095  csbie2t  3097  sbcco3g  3106  csbco3g  3107  dfnfc2  3814  eusvnfb  4439  eusv2i  4440  peano2  4579  iota2d  5185  iota2  5188  fmptcof  5663  riota5f  5833  riota5  5834  fmpoco  6195  nfixpxy  6695  nfnegd  8115  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsum  10456  fprodeq0g  11601  pcmpt  12295  strcollnft  14019
  Copyright terms: Public domain W3C validator