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

Theorem brdif 4263
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 3332 . 2  |-  ( <. A ,  B >.  e.  ( R  \  S
)  <->  ( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
2 df-br 4216 . 2  |-  ( A ( R  \  S
) B  <->  <. A ,  B >.  e.  ( R 
\  S ) )
3 df-br 4216 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4216 . . . 4  |-  ( A S B  <->  <. A ,  B >.  e.  S )
54notbii 289 . . 3  |-  ( -.  A S B  <->  -.  <. A ,  B >.  e.  S )
63, 5anbi12i 680 . 2  |-  ( ( A R B  /\  -.  A S B )  <-> 
( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
71, 2, 63bitr4i 270 1  |-  ( A ( R  \  S
) B  <->  ( A R B  /\  -.  A S B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178    /\ wa 360    e. wcel 1726    \ cdif 3319   <.cop 3819   class class class wbr 4215
This theorem is referenced by:  fndmdif  5837  isocnv3  6055  brdifun  6935  dfsup2OLD  7451  dflt2  10746  pltval  14422  dftr6  25378  dffr5  25381  fundmpss  25395  brsset  25739  dfon3  25742  brtxpsd2  25745  dffun10  25764  elfuns  25765  dfrdg4  25800  dfint3  25802  brub  25804  broutsideof  26060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-br 4216
  Copyright terms: Public domain W3C validator