# Metamath Proof Explorer

## Theorem cnvun

Description: The converse of a union is the union of converses. Theorem 16 of Suppes p. 62. (Contributed by NM, 25-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion cnvun ${⊢}{\left({A}\cup {B}\right)}^{-1}={{A}}^{-1}\cup {{B}}^{-1}$

### Proof

Step Hyp Ref Expression
1 df-cnv ${⊢}{\left({A}\cup {B}\right)}^{-1}=\left\{⟨{x},{y}⟩|{y}\left({A}\cup {B}\right){x}\right\}$
2 unopab ${⊢}\left\{⟨{x},{y}⟩|{y}{A}{x}\right\}\cup \left\{⟨{x},{y}⟩|{y}{B}{x}\right\}=\left\{⟨{x},{y}⟩|\left({y}{A}{x}\vee {y}{B}{x}\right)\right\}$
3 brun ${⊢}{y}\left({A}\cup {B}\right){x}↔\left({y}{A}{x}\vee {y}{B}{x}\right)$
4 3 opabbii ${⊢}\left\{⟨{x},{y}⟩|{y}\left({A}\cup {B}\right){x}\right\}=\left\{⟨{x},{y}⟩|\left({y}{A}{x}\vee {y}{B}{x}\right)\right\}$
5 2 4 eqtr4i ${⊢}\left\{⟨{x},{y}⟩|{y}{A}{x}\right\}\cup \left\{⟨{x},{y}⟩|{y}{B}{x}\right\}=\left\{⟨{x},{y}⟩|{y}\left({A}\cup {B}\right){x}\right\}$
6 1 5 eqtr4i ${⊢}{\left({A}\cup {B}\right)}^{-1}=\left\{⟨{x},{y}⟩|{y}{A}{x}\right\}\cup \left\{⟨{x},{y}⟩|{y}{B}{x}\right\}$
7 df-cnv ${⊢}{{A}}^{-1}=\left\{⟨{x},{y}⟩|{y}{A}{x}\right\}$
8 df-cnv ${⊢}{{B}}^{-1}=\left\{⟨{x},{y}⟩|{y}{B}{x}\right\}$
9 7 8 uneq12i ${⊢}{{A}}^{-1}\cup {{B}}^{-1}=\left\{⟨{x},{y}⟩|{y}{A}{x}\right\}\cup \left\{⟨{x},{y}⟩|{y}{B}{x}\right\}$
10 6 9 eqtr4i ${⊢}{\left({A}\cup {B}\right)}^{-1}={{A}}^{-1}\cup {{B}}^{-1}$