![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brun | Structured version Visualization version GIF version |
Description: The union of two binary relations. (Contributed by NM, 21-Dec-2008.) |
Ref | Expression |
---|---|
brun | ⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elun 4076 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ∪ 𝑆) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∨ 〈𝐴, 𝐵〉 ∈ 𝑆)) | |
2 | df-br 5031 | . 2 ⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑅 ∪ 𝑆)) | |
3 | df-br 5031 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
4 | df-br 5031 | . . 3 ⊢ (𝐴𝑆𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑆) | |
5 | 3, 4 | orbi12i 912 | . 2 ⊢ ((𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵) ↔ (〈𝐴, 𝐵〉 ∈ 𝑅 ∨ 〈𝐴, 𝐵〉 ∈ 𝑆)) |
6 | 1, 2, 5 | 3bitr4i 306 | 1 ⊢ (𝐴(𝑅 ∪ 𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑆𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∨ wo 844 ∈ wcel 2111 ∪ cun 3879 〈cop 4531 class class class wbr 5030 |
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 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-br 5031 |
This theorem is referenced by: dmun 5743 qfto 5948 poleloe 5958 cnvun 5968 coundi 6067 coundir 6068 fununmo 6371 brdifun 8301 fpwwe2lem13 10053 ltxrlt 10700 ltxr 12498 dfle2 12528 brprop 30457 satfbrsuc 32726 dfso2 33103 eqfunresadj 33117 dfon3 33466 brcup 33513 dfrdg4 33525 dffrege99 40663 |
Copyright terms: Public domain | W3C validator |