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

Theorem brun 4069
Description: The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
Assertion
Ref Expression
brun  |-  ( A ( R  u.  S
) B  <->  ( A R B  \/  A S B ) )

Proof of Theorem brun
StepHypRef Expression
1 elun 3316 . 2  |-  ( <. A ,  B >.  e.  ( R  u.  S
)  <->  ( <. A ,  B >.  e.  R  \/  <. A ,  B >.  e.  S ) )
2 df-br 4024 . 2  |-  ( A ( R  u.  S
) B  <->  <. A ,  B >.  e.  ( R  u.  S ) )
3 df-br 4024 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4024 . . 3  |-  ( A S B  <->  <. A ,  B >.  e.  S )
53, 4orbi12i 507 . 2  |-  ( ( A R B  \/  A S B )  <->  ( <. A ,  B >.  e.  R  \/  <. A ,  B >.  e.  S ) )
61, 2, 53bitr4i 268 1  |-  ( A ( R  u.  S
) B  <->  ( A R B  \/  A S B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    e. wcel 1684    u. cun 3150   <.cop 3643   class class class wbr 4023
This theorem is referenced by:  dmun  4885  qfto  5064  poleloe  5077  cnvun  5086  coundi  5174  coundir  5175  brdifun  6687  fpwwe2lem13  8264  ltxrlt  8893  ltxr  10457  dfle2  10481  dfso2  24111  dfon3  24432  brcup  24478  dfrdg4  24488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-br 4024
  Copyright terms: Public domain W3C validator