MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvun Structured version   Visualization version   GIF version

Theorem cnvun 6099
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.)
Assertion
Ref Expression
cnvun (𝐴𝐵) = (𝐴𝐵)

Proof of Theorem cnvun
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-cnv 5645 . . 3 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴𝐵)𝑥}
2 unopab 5191 . . . 4 ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥𝑦𝐵𝑥)}
3 brun 5160 . . . . 5 (𝑦(𝐴𝐵)𝑥 ↔ (𝑦𝐴𝑥𝑦𝐵𝑥))
43opabbii 5176 . . . 4 {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴𝐵)𝑥} = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥𝑦𝐵𝑥)}
52, 4eqtr4i 2764 . . 3 ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴𝐵)𝑥}
61, 5eqtr4i 2764 . 2 (𝐴𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
7 df-cnv 5645 . . 3 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
8 df-cnv 5645 . . 3 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
97, 8uneq12i 4125 . 2 (𝐴𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
106, 9eqtr4i 2764 1 (𝐴𝐵) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 846   = wceq 1542  cun 3912   class class class wbr 5109  {copab 5171  ccnv 5636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-un 3919  df-br 5110  df-opab 5172  df-cnv 5645
This theorem is referenced by:  rnun  6102  funcnvpr  6567  funcnvtp  6568  funcnvqp  6569  f1oun  6807  f1oprswap  6832  suppun  8119  sbthlem8  9040  domss2  9086  cnvfi  9130  1sdomOLD  9199  fsuppun  9332  fpwwe2lem12  10586  trclublem  14889  mbfres2  25032  ex-cnv  29430  cnvprop  31664  padct  31690  cycpmconjslem2  32060  eulerpartlemt  33035  mthmpps  34240  clcnvlem  41987  frege131d  42128
  Copyright terms: Public domain W3C validator