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

Theorem brdif 4363
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 3359 . 2  |-  ( <. A ,  B >.  e.  ( R  \  S
)  <->  ( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
2 df-br 4314 . 2  |-  ( A ( R  \  S
) B  <->  <. A ,  B >.  e.  ( R 
\  S ) )
3 df-br 4314 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4314 . . . 4  |-  ( A S B  <->  <. A ,  B >.  e.  S )
54notbii 296 . . 3  |-  ( -.  A S B  <->  -.  <. A ,  B >.  e.  S )
63, 5anbi12i 697 . 2  |-  ( ( A R B  /\  -.  A S B )  <-> 
( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
71, 2, 63bitr4i 277 1  |-  ( A ( R  \  S
) B  <->  ( A R B  /\  -.  A S B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    /\ wa 369    e. wcel 1756    \ cdif 3346   <.cop 3904   class class class wbr 4313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-dif 3352  df-br 4314
This theorem is referenced by:  fndmdif  5828  isocnv3  6044  brdifun  7149  dfsup2OLD  7714  dflt2  11146  pltval  15151  dftr6  27582  dffr5  27585  fundmpss  27599  brsset  27942  dfon3  27945  brtxpsd2  27948  dffun10  27967  elfuns  27968  dfrdg4  28003  dfint3  28005  brub  28007  broutsideof  28174
  Copyright terms: Public domain W3C validator