This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvun

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)

Ref Expression
Assertion cnvun 
|- `' ( A u. B ) = ( `' A u. `' B )

Proof

Step Hyp Ref Expression
1 df-cnv 
 |-  `' ( A u. B ) = { <. x , y >. | y ( A u. B ) x }
2 unopab 
 |-  ( { <. x , y >. | y A x } u. { <. x , y >. | y B x } ) = { <. x , y >. | ( y A x \/ y B x ) }
3 brun 
 |-  ( y ( A u. B ) x <-> ( y A x \/ y B x ) )
4 3 opabbii 
 |-  { <. x , y >. | y ( A u. B ) x } = { <. x , y >. | ( y A x \/ y B x ) }
5 2 4 eqtr4i 
 |-  ( { <. x , y >. | y A x } u. { <. x , y >. | y B x } ) = { <. x , y >. | y ( A u. B ) x }
6 1 5 eqtr4i 
 |-  `' ( A u. B ) = ( { <. x , y >. | y A x } u. { <. x , y >. | y B x } )
7 df-cnv 
 |-  `' A = { <. x , y >. | y A x }
8 df-cnv 
 |-  `' B = { <. x , y >. | y B x }
9 7 8 uneq12i 
 |-  ( `' A u. `' B ) = ( { <. x , y >. | y A x } u. { <. x , y >. | y B x } )
10 6 9 eqtr4i 
 |-  `' ( A u. B ) = ( `' A u. `' B )