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

Theorem brun 5161
Description: The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
Assertion
Ref Expression
brun (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))

Proof of Theorem brun
StepHypRef Expression
1 elun 4113 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∨ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2 df-br 5111 . 2 (𝐴(𝑅𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅𝑆))
3 df-br 5111 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4 df-br 5111 . . 3 (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
53, 4orbi12i 914 . 2 ((𝐴𝑅𝐵𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∨ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
61, 2, 53bitr4i 303 1 (𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wo 846  wcel 2107  cun 3913  cop 4597   class class class wbr 5110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-br 5111
This theorem is referenced by:  dmun  5871  qfto  6080  poleloe  6090  cnvun  6100  coundi  6204  coundir  6205  fununmo  6553  eqfunresadj  7310  brdifun  8684  fpwwe2lem12  10585  ltxrlt  11232  ltxr  13043  dfle2  13073  brprop  31653  satfbrsuc  34000  dfso2  34367  dfon3  34506  brcup  34553  dfrdg4  34565  dffrege99  42308
  Copyright terms: Public domain W3C validator