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

Theorem eldifd 3051
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3050. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
eldifd.1  |-  ( ph  ->  A  e.  B )
eldifd.2  |-  ( ph  ->  -.  A  e.  C
)
Assertion
Ref Expression
eldifd  |-  ( ph  ->  A  e.  ( B 
\  C ) )

Proof of Theorem eldifd
StepHypRef Expression
1 eldifd.1 . 2  |-  ( ph  ->  A  e.  B )
2 eldifd.2 . 2  |-  ( ph  ->  -.  A  e.  C
)
3 eldif 3050 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
41, 2, 3sylanbrc 413 1  |-  ( ph  ->  A  e.  ( B 
\  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1465    \ cdif 3038
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-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-dif 3043
This theorem is referenced by:  exmidundif  4099  exmidundifim  4100  frirrg  4242  dcdifsnid  6368  phpelm  6728  findcard2d  6753  findcard2sd  6754  diffifi  6756  unsnfidcex  6776  unsnfidcel  6777  undifdcss  6779  difinfsnlem  6952  difinfsn  6953  hashunlem  10505  seq3coll  10540  fsum3cvg  11101  isumss  11115  fisumss  11116
  Copyright terms: Public domain W3C validator