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

Theorem brdif 4452
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 3413 . 2  |-  ( <. A ,  B >.  e.  ( R  \  S
)  <->  ( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
2 df-br 4402 . 2  |-  ( A ( R  \  S
) B  <->  <. A ,  B >.  e.  ( R 
\  S ) )
3 df-br 4402 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4402 . . . 4  |-  ( A S B  <->  <. A ,  B >.  e.  S )
54notbii 298 . . 3  |-  ( -.  A S B  <->  -.  <. A ,  B >.  e.  S )
63, 5anbi12i 702 . 2  |-  ( ( A R B  /\  -.  A S B )  <-> 
( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
71, 2, 63bitr4i 281 1  |-  ( A ( R  \  S
) B  <->  ( A R B  /\  -.  A S B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188    /\ wa 371    e. wcel 1886    \ cdif 3400   <.cop 3973   class class class wbr 4401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-dif 3406  df-br 4402
This theorem is referenced by:  fndmdif  5984  isocnv3  6221  brdifun  7387  dflt2  11444  pltval  16199  ltgov  24635  opeldifid  28203  qtophaus  28656  dftr6  30383  dffr5  30386  fundmpss  30400  brsset  30649  dfon3  30652  brtxpsd2  30655  dffun10  30674  elfuns  30675  dfrecs2  30710  dfrdg4  30711  dfint3  30712  brub  30714  broutsideof  30881  frege124d  36347
  Copyright terms: Public domain W3C validator