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

Theorem cnvun 5340
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 4946 . . 3  |-  `' ( A  u.  B )  =  { <. x ,  y >.  |  y ( A  u.  B
) x }
2 unopab 4465 . . . 4  |-  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )  =  { <. x ,  y >.  |  ( y A x  \/  y B x ) }
3 brun 4438 . . . . 5  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
43opabbii 4454 . . . 4  |-  { <. x ,  y >.  |  y ( A  u.  B
) x }  =  { <. x ,  y
>.  |  ( y A x  \/  y B x ) }
52, 4eqtr4i 2483 . . 3  |-  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )  =  { <. x ,  y >.  |  y ( A  u.  B
) x }
61, 5eqtr4i 2483 . 2  |-  `' ( A  u.  B )  =  ( { <. x ,  y >.  |  y A x }  u.  {
<. x ,  y >.  |  y B x } )
7 df-cnv 4946 . . 3  |-  `' A  =  { <. x ,  y
>.  |  y A x }
8 df-cnv 4946 . . 3  |-  `' B  =  { <. x ,  y
>.  |  y B x }
97, 8uneq12i 3606 . 2  |-  ( `' A  u.  `' B
)  =  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )
106, 9eqtr4i 2483 1  |-  `' ( A  u.  B )  =  ( `' A  u.  `' B )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    = wceq 1370    u. cun 3424   class class class wbr 4390   {copab 4447   `'ccnv 4937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-un 3431  df-br 4391  df-opab 4449  df-cnv 4946
This theorem is referenced by:  rnun  5343  f1oun  5758  f1oprswap  5778  suppun  6809  sbthlem8  7528  domss2  7570  1sdom  7616  fsuppun  7740  fpwwe2lem13  8910  strlemor1  14367  xpsc  14597  gsumzaddlemOLD  16514  funsnfsupOLD  17777  mbfres2  21239  constr2spthlem1  23628  constr3pthlem2  23677  ex-cnv  23779  eulerpartlemt  26888
  Copyright terms: Public domain W3C validator