| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cnvun | Structured version Visualization version GIF version | ||
| 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 |
|---|---|
| cnvun | ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-cnv 5693 | . . 3 ⊢ ◡(𝐴 ∪ 𝐵) = {〈𝑥, 𝑦〉 ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} | |
| 2 | unopab 5224 | . . . 4 ⊢ ({〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ∪ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) = {〈𝑥, 𝑦〉 ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)} | |
| 3 | brun 5194 | . . . . 5 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) | |
| 4 | 3 | opabbii 5210 | . . . 4 ⊢ {〈𝑥, 𝑦〉 ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} = {〈𝑥, 𝑦〉 ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)} |
| 5 | 2, 4 | eqtr4i 2768 | . . 3 ⊢ ({〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ∪ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) = {〈𝑥, 𝑦〉 ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} |
| 6 | 1, 5 | eqtr4i 2768 | . 2 ⊢ ◡(𝐴 ∪ 𝐵) = ({〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ∪ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
| 7 | df-cnv 5693 | . . 3 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
| 8 | df-cnv 5693 | . . 3 ⊢ ◡𝐵 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥} | |
| 9 | 7, 8 | uneq12i 4166 | . 2 ⊢ (◡𝐴 ∪ ◡𝐵) = ({〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ∪ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
| 10 | 6, 9 | eqtr4i 2768 | 1 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ∨ wo 848 = wceq 1540 ∪ cun 3949 class class class wbr 5143 {copab 5205 ◡ccnv 5684 |
| 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 df-opab 5206 df-cnv 5693 |
| This theorem is referenced by: rnun 6165 funcnvpr 6628 funcnvtp 6629 funcnvqp 6630 f1oun 6867 f1oprswap 6892 suppun 8209 sbthlem8 9130 domss2 9176 cnvfi 9216 1sdomOLD 9285 fsuppun 9427 fpwwe2lem12 10682 trclublem 15034 mbfres2 25680 ex-cnv 30456 suppun2 32693 cnvprop 32705 padct 32731 cycpmconjslem2 33175 eulerpartlemt 34373 mthmpps 35587 clcnvlem 43636 frege131d 43777 |
| Copyright terms: Public domain | W3C validator |