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

Theorem brdif 4446
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 3400 . 2  |-  ( <. A ,  B >.  e.  ( R  \  S
)  <->  ( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
2 df-br 4396 . 2  |-  ( A ( R  \  S
) B  <->  <. A ,  B >.  e.  ( R 
\  S ) )
3 df-br 4396 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4396 . . . 4  |-  ( A S B  <->  <. A ,  B >.  e.  S )
54notbii 303 . . 3  |-  ( -.  A S B  <->  -.  <. A ,  B >.  e.  S )
63, 5anbi12i 711 . 2  |-  ( ( A R B  /\  -.  A S B )  <-> 
( <. A ,  B >.  e.  R  /\  -.  <. A ,  B >.  e.  S ) )
71, 2, 63bitr4i 285 1  |-  ( A ( R  \  S
) B  <->  ( A R B  /\  -.  A S B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189    /\ wa 376    e. wcel 1904    \ cdif 3387   <.cop 3965   class class class wbr 4395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393  df-br 4396
This theorem is referenced by:  fndmdif  6001  isocnv3  6241  brdifun  7408  dflt2  11470  pltval  16284  ltgov  24721  opeldifid  28286  qtophaus  28737  dftr6  30461  dffr5  30464  fundmpss  30478  brsset  30727  dfon3  30730  brtxpsd2  30733  dffun10  30752  elfuns  30753  dfrecs2  30788  dfrdg4  30789  dfint3  30790  brub  30792  broutsideof  30959  frege124d  36424
  Copyright terms: Public domain W3C validator