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

Theorem nfcvd 2195
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 2194 . 2  |-  F/_ x A
21a1i 9 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2181
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-17 1435
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-nfc 2183
This theorem is referenced by:  nfeld  2209  vtoclgft  2621  vtocld  2623  sbcralt  2862  sbcrext  2863  csbied  2920  csbie2t  2922  sbcco3g  2931  csbco3g  2932  dfnfc2  3626  eusvnfb  4214  eusv2i  4215  peano2  4346  iota2d  4920  iota2  4921  fmptcof  5359  riota5f  5520  riota5  5521  fmpt2co  5865  nfnegd  7270  strcollnft  10496
  Copyright terms: Public domain W3C validator