Theorem brun 5194

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 4153	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ∪ 𝑆) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∨ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
2		df-br 5144	. 2 ⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ∪ 𝑆))
3		df-br 5144	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
4		df-br 5144	. . 3 ⊢ (𝐴𝑆𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑆)
5	3, 4	orbi12i 915	. 2 ⊢ ((𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ∨ ⟨𝐴, 𝐵⟩ ∈ 𝑆))
6	1, 2, 5	3bitr4i 303	1 ⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵))

Syntax hints:   ↔ wb 206   ∨ wo 848   ∈ wcel 2108   ∪ cun 3949  ⟨cop 4632   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-br 5144

This theorem is referenced by:  dmun  5921  qfto  6141  poleloe  6151  cnvun  6162  coundi  6267  coundir  6268  fununmo  6613  eqfunresadj  7380  brdifun  8775  fpwwe2lem12  10682  ltxrlt  11331  ltxr  13157  dfle2  13189  brprop  32706  satfbrsuc  35371  dfso2  35755  dfon3  35893  brcup  35940  dfrdg4  35952  dffrege99  43975