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

Theorem brun 4487
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 3631 . 2  |-  ( <. A ,  B >.  e.  ( R  u.  S
)  <->  ( <. A ,  B >.  e.  R  \/  <. A ,  B >.  e.  S ) )
2 df-br 4440 . 2  |-  ( A ( R  u.  S
) B  <->  <. A ,  B >.  e.  ( R  u.  S ) )
3 df-br 4440 . . 3  |-  ( A R B  <->  <. A ,  B >.  e.  R )
4 df-br 4440 . . 3  |-  ( A S B  <->  <. A ,  B >.  e.  S )
53, 4orbi12i 519 . 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 366    e. wcel 1823    u. cun 3459   <.cop 4022   class class class wbr 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-br 4440
This theorem is referenced by:  dmun  5198  qfto  5376  poleloe  5386  cnvun  5396  coundi  5491  coundir  5492  fununmo  5613  brdifun  7330  fpwwe2lem13  9009  ltxrlt  9644  ltxr  11327  dfle2  11356  dfso2  29424  dfon3  29770  brcup  29817  dfrdg4  29828
  Copyright terms: Public domain W3C validator