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

Theorem cnvun 5256
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  |-  `' ( A  u.  B )  =  ( `' A  u.  `' B )

Proof of Theorem cnvun
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-cnv 4857 . . 3  |-  `' ( A  u.  B )  =  { <. x ,  y >.  |  y ( A  u.  B
) x }
2 unopab 4496 . . . 4  |-  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )  =  { <. x ,  y >.  |  ( y A x  \/  y B x ) }
3 brun 4469 . . . . 5  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
43opabbii 4485 . . . 4  |-  { <. x ,  y >.  |  y ( A  u.  B
) x }  =  { <. x ,  y
>.  |  ( y A x  \/  y B x ) }
52, 4eqtr4i 2454 . . 3  |-  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )  =  { <. x ,  y >.  |  y ( A  u.  B
) x }
61, 5eqtr4i 2454 . 2  |-  `' ( A  u.  B )  =  ( { <. x ,  y >.  |  y A x }  u.  {
<. x ,  y >.  |  y B x } )
7 df-cnv 4857 . . 3  |-  `' A  =  { <. x ,  y
>.  |  y A x }
8 df-cnv 4857 . . 3  |-  `' B  =  { <. x ,  y
>.  |  y B x }
97, 8uneq12i 3618 . 2  |-  ( `' A  u.  `' B
)  =  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )
106, 9eqtr4i 2454 1  |-  `' ( A  u.  B )  =  ( `' A  u.  `' B )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 369    = wceq 1437    u. cun 3434   class class class wbr 4420   {copab 4478   `'ccnv 4848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-un 3441  df-br 4421  df-opab 4480  df-cnv 4857
This theorem is referenced by:  rnun  5259  f1oun  5846  f1oprswap  5866  suppun  6942  sbthlem8  7691  domss2  7733  1sdom  7777  fsuppun  7904  fpwwe2lem13  9067  trclublem  13047  strlemor1  15204  xpsc  15450  mbfres2  22587  constr2spthlem1  25309  constr3pthlem2  25369  ex-cnv  25872  padct  28300  eulerpartlemt  29199  mthmpps  30215  frege131d  36215
  Copyright terms: Public domain W3C validator