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

Theorem cnvun 5260
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 4861 . . 3  |-  `' ( A  u.  B )  =  { <. x ,  y >.  |  y ( A  u.  B
) x }
2 unopab 4492 . . . 4  |-  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )  =  { <. x ,  y >.  |  ( y A x  \/  y B x ) }
3 brun 4465 . . . . 5  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
43opabbii 4481 . . . 4  |-  { <. x ,  y >.  |  y ( A  u.  B
) x }  =  { <. x ,  y
>.  |  ( y A x  \/  y B x ) }
52, 4eqtr4i 2487 . . 3  |-  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )  =  { <. x ,  y >.  |  y ( A  u.  B
) x }
61, 5eqtr4i 2487 . 2  |-  `' ( A  u.  B )  =  ( { <. x ,  y >.  |  y A x }  u.  {
<. x ,  y >.  |  y B x } )
7 df-cnv 4861 . . 3  |-  `' A  =  { <. x ,  y
>.  |  y A x }
8 df-cnv 4861 . . 3  |-  `' B  =  { <. x ,  y
>.  |  y B x }
97, 8uneq12i 3598 . 2  |-  ( `' A  u.  `' B
)  =  ( {
<. x ,  y >.  |  y A x }  u.  { <. x ,  y >.  |  y B x } )
106, 9eqtr4i 2487 1  |-  `' ( A  u.  B )  =  ( `' A  u.  `' B )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 374    = wceq 1455    u. cun 3414   class class class wbr 4416   {copab 4474   `'ccnv 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-br 4417  df-opab 4476  df-cnv 4861
This theorem is referenced by:  rnun  5263  funcnvpr  5658  funcnvtp  5659  funcnvqp  5660  f1oun  5856  f1oprswap  5877  suppun  6962  sbthlem8  7715  domss2  7757  1sdom  7801  fsuppun  7928  fpwwe2lem13  9093  trclublem  13108  strlemor1  15266  xpsc  15512  mbfres2  22650  constr2spthlem1  25373  constr3pthlem2  25433  ex-cnv  25936  padct  28356  eulerpartlemt  29253  mthmpps  30269  clcnvlem  36275  frege131d  36401
  Copyright terms: Public domain W3C validator