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

Theorem nfcvd 2226
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 2225 . 2  |-  F/_ x A
21a1i 9 1  |-  ( ph  -> 
F/_ x A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/_wnfc 2212
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1381  ax-17 1462
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-nfc 2214
This theorem is referenced by:  nfeld  2240  vtoclgft  2663  vtocld  2665  sbcralt  2904  sbcrext  2905  csbied  2963  csbie2t  2965  sbcco3g  2974  csbco3g  2975  dfnfc2  3654  eusvnfb  4250  eusv2i  4251  peano2  4383  iota2d  4971  iota2  4972  fmptcof  5428  riota5f  5593  riota5  5594  fmpt2co  5938  nfnegd  7622  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemfvp  9830  iseqf1olemqsum  9833  strcollnft  11317
  Copyright terms: Public domain W3C validator