Theorem brun 5083

Description: The union of two binary relations. (Contributed by NM, 21-Dec-2008.)

Assertion

Ref	Expression
brun	⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵))

Proof of Theorem brun

Step	Hyp	Ref	Expression
1		elun 4054	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∪ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∨ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5033	. 2 ⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∪ 𝑆))
3		df-br 5033	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5033	. . 3 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	3, 4	orbi12i 912	. 2 ⊢ ((𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∨ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
6	1, 2, 5	3bitr4i 306	1 ⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵))

Syntax hints:   ↔ wb 209   ∨ wo 844   ∈ wcel 2111   ∪ cun 3856  ⟨cop 4528   class class class wbr 5032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-br 5033

This theorem is referenced by:  dmun  5750  qfto  5953  poleloe  5963  cnvun  5973  coundi  6077  coundir  6078  fununmo  6382  brdifun  8328  fpwwe2lem12  10102  ltxrlt  10749  ltxr  12551  dfle2  12581  brprop  30554  satfbrsuc  32844  dfso2  33237  eqfunresadj  33251  dfon3  33743  brcup  33790  dfrdg4  33802  dffrege99  41036