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

Theorem cnvun 5396
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 4996 . . 3  |-  `' ( A  u.  B )  =  { <. x ,  y >.  |  y ( A  u.  B
) x }
2 unopab 4514 . . . 4  |-  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )  =  { <. x ,  y >.  |  ( y A x  \/  y B x ) }
3 brun 4487 . . . . 5  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
43opabbii 4503 . . . 4  |-  { <. x ,  y >.  |  y ( A  u.  B
) x }  =  { <. x ,  y
>.  |  ( y A x  \/  y B x ) }
52, 4eqtr4i 2486 . . 3  |-  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )  =  { <. x ,  y >.  |  y ( A  u.  B
) x }
61, 5eqtr4i 2486 . 2  |-  `' ( A  u.  B )  =  ( { <. x ,  y >.  |  y A x }  u.  {
<. x ,  y >.  |  y B x } )
7 df-cnv 4996 . . 3  |-  `' A  =  { <. x ,  y
>.  |  y A x }
8 df-cnv 4996 . . 3  |-  `' B  =  { <. x ,  y
>.  |  y B x }
97, 8uneq12i 3642 . 2  |-  ( `' A  u.  `' B
)  =  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )
106, 9eqtr4i 2486 1  |-  `' ( A  u.  B )  =  ( `' A  u.  `' B )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 366    = wceq 1398    u. cun 3459   class class class wbr 4439   {copab 4496   `'ccnv 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-br 4440  df-opab 4498  df-cnv 4996
This theorem is referenced by:  rnun  5399  f1oun  5817  f1oprswap  5837  suppun  6912  sbthlem8  7627  domss2  7669  1sdom  7715  fsuppun  7840  fpwwe2lem13  9009  trclublem  12916  strlemor1  14814  xpsc  15049  gsumzaddlemOLD  17138  funsnfsupOLD  18454  mbfres2  22221  constr2spthlem1  24801  constr3pthlem2  24861  ex-cnv  25363  padct  27779  eulerpartlemt  28577  mthmpps  29209
  Copyright terms: Public domain W3C validator