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 5046 | . . 3 ⊢ ◡(𝐴 ∪ 𝐵) = {〈𝑥, 𝑦〉 ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} | |
2 | unopab 4660 | . . . 4 ⊢ ({〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ∪ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) = {〈𝑥, 𝑦〉 ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)} | |
3 | brun 4633 | . . . . 5 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) | |
4 | 3 | opabbii 4649 | . . . 4 ⊢ {〈𝑥, 𝑦〉 ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} = {〈𝑥, 𝑦〉 ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)} |
5 | 2, 4 | eqtr4i 2635 | . . 3 ⊢ ({〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ∪ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) = {〈𝑥, 𝑦〉 ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} |
6 | 1, 5 | eqtr4i 2635 | . 2 ⊢ ◡(𝐴 ∪ 𝐵) = ({〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ∪ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
7 | df-cnv 5046 | . . 3 ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | |
8 | df-cnv 5046 | . . 3 ⊢ ◡𝐵 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥} | |
9 | 7, 8 | uneq12i 3727 | . 2 ⊢ (◡𝐴 ∪ ◡𝐵) = ({〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} ∪ {〈𝑥, 𝑦〉 ∣ 𝑦𝐵𝑥}) |
10 | 6, 9 | eqtr4i 2635 | 1 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 382 = wceq 1475 ∪ cun 3538 class class class wbr 4583 {copab 4642 ◡ccnv 5037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-br 4584 df-opab 4644 df-cnv 5046 |
This theorem is referenced by: rnun 5460 funcnvpr 5864 funcnvtp 5865 funcnvqp 5866 funcnvqpOLD 5867 f1oun 6069 f1oprswap 6092 suppun 7202 sbthlem8 7962 domss2 8004 1sdom 8048 fsuppun 8177 fpwwe2lem13 9343 trclublem 13582 strlemor1 15796 xpsc 16040 mbfres2 23218 constr2spthlem1 26124 constr3pthlem2 26184 ex-cnv 26686 padct 28885 eulerpartlemt 29760 mthmpps 30733 clcnvlem 36949 frege131d 37075 |
Copyright terms: Public domain | W3C validator |