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

Theorem brun 4435
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 3592 . 2  |-  ( <. A ,  B >.  e.  ( R  u.  S
)  <->  ( <. A ,  B >.  e.  R  \/  <. A ,  B >.  e.  S ) )
2 df-br 4388 . 2  |-  ( A ( R  u.  S
) B  <->  <. A ,  B >.  e.  ( R  u.  S ) )
3 df-br 4388 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4388 . . 3  |-  ( A S B  <->  <. A ,  B >.  e.  S )
53, 4orbi12i 521 . 2  |-  ( ( A R B  \/  A S B )  <->  ( <. A ,  B >.  e.  R  \/  <. A ,  B >.  e.  S ) )
61, 2, 53bitr4i 277 1  |-  ( A ( R  u.  S
) B  <->  ( A R B  \/  A S B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368    e. wcel 1758    u. cun 3421   <.cop 3978   class class class wbr 4387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-v 3067  df-un 3428  df-br 4388
This theorem is referenced by:  dmun  5141  qfto  5314  poleloe  5327  cnvun  5337  coundi  5434  coundir  5435  fununmo  5556  brdifun  7225  fpwwe2lem13  8907  ltxrlt  9543  ltxr  11193  dfle2  11222  dfso2  27695  dfon3  28054  brcup  28101  dfrdg4  28112
  Copyright terms: Public domain W3C validator