MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brdif Unicode version

Theorem brdif 4152
Description: The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
Assertion
Ref Expression
brdif  |-  ( A ( R  \  S
) B  <->  ( A R B  /\  -.  A S B ) )

Proof of Theorem brdif
StepHypRef Expression
1 eldif 3238 . 2  |-  ( <. A ,  B >.  e.  ( R  \  S
)  <->  ( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
2 df-br 4105 . 2  |-  ( A ( R  \  S
) B  <->  <. A ,  B >.  e.  ( R 
\  S ) )
3 df-br 4105 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4105 . . . 4  |-  ( A S B  <->  <. A ,  B >.  e.  S )
54notbii 287 . . 3  |-  ( -.  A S B  <->  -.  <. A ,  B >.  e.  S )
63, 5anbi12i 678 . 2  |-  ( ( A R B  /\  -.  A S B )  <-> 
( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
71, 2, 63bitr4i 268 1  |-  ( A ( R  \  S
) B  <->  ( A R B  /\  -.  A S B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    /\ wa 358    e. wcel 1710    \ cdif 3225   <.cop 3719   class class class wbr 4104
This theorem is referenced by:  fndmdif  5712  isocnv3  5916  brdifun  6774  dfsup2OLD  7286  dflt2  10574  pltval  14193  dftr6  24665  dffr5  24668  fundmpss  24680  brsset  24987  dfon3  24990  brtxpsd2  24993  dffun10  25011  elfuns  25012  dfrdg4  25047  broutsideof  25303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-dif 3231  df-br 4105
  Copyright terms: Public domain W3C validator