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

Theorem cnvun 6142
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 5684 . . 3 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴𝐵)𝑥}
2 unopab 5230 . . . 4 ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥𝑦𝐵𝑥)}
3 brun 5199 . . . . 5 (𝑦(𝐴𝐵)𝑥 ↔ (𝑦𝐴𝑥𝑦𝐵𝑥))
43opabbii 5215 . . . 4 {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴𝐵)𝑥} = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥𝑦𝐵𝑥)}
52, 4eqtr4i 2763 . . 3 ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴𝐵)𝑥}
61, 5eqtr4i 2763 . 2 (𝐴𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
7 df-cnv 5684 . . 3 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
8 df-cnv 5684 . . 3 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
97, 8uneq12i 4161 . 2 (𝐴𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
106, 9eqtr4i 2763 1 (𝐴𝐵) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 845   = wceq 1541  cun 3946   class class class wbr 5148  {copab 5210  ccnv 5675
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-br 5149  df-opab 5211  df-cnv 5684
This theorem is referenced by:  rnun  6145  funcnvpr  6610  funcnvtp  6611  funcnvqp  6612  f1oun  6852  f1oprswap  6877  suppun  8168  sbthlem8  9089  domss2  9135  cnvfi  9179  1sdomOLD  9248  fsuppun  9381  fpwwe2lem12  10636  trclublem  14941  mbfres2  25161  ex-cnv  29687  cnvprop  31913  padct  31939  cycpmconjslem2  32309  eulerpartlemt  33365  mthmpps  34568  clcnvlem  42364  frege131d  42505
  Copyright terms: Public domain W3C validator