Metamath Proof Explorer

Theorem dmun

Description: The domain of a union is the union of domains. Exercise 56(a) of Enderton p. 65. (Contributed by NM, 12-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dmun 
|- dom ( A u. B ) = ( dom A u. dom B )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = z -> ( y A x <-> z A x ) )
2 1 exbidv 
 |-  ( y = z -> ( E. x y A x <-> E. x z A x ) )
3 breq1 
 |-  ( y = z -> ( y B x <-> z B x ) )
4 3 exbidv 
 |-  ( y = z -> ( E. x y B x <-> E. x z B x ) )
5 2 4 unabw 
 |-  ( { y | E. x y A x } u. { y | E. x y B x } ) = { z | ( E. x z A x \/ E. x z B x ) }
6 brun 
 |-  ( z ( A u. B ) x <-> ( z A x \/ z B x ) )
7 6 exbii 
 |-  ( E. x z ( A u. B ) x <-> E. x ( z A x \/ z B x ) )
8 19.43 
 |-  ( E. x ( z A x \/ z B x ) <-> ( E. x z A x \/ E. x z B x ) )
9 7 8 bitr2i 
 |-  ( ( E. x z A x \/ E. x z B x ) <-> E. x z ( A u. B ) x )
10 9 abbii 
 |-  { z | ( E. x z A x \/ E. x z B x ) } = { z | E. x z ( A u. B ) x }
11 5 10 eqtri 
 |-  ( { y | E. x y A x } u. { y | E. x y B x } ) = { z | E. x z ( A u. B ) x }
12 df-dm 
 |-  dom A = { y | E. x y A x }
13 df-dm 
 |-  dom B = { y | E. x y B x }
14 12 13 uneq12i 
 |-  ( dom A u. dom B ) = ( { y | E. x y A x } u. { y | E. x y B x } )
15 df-dm 
 |-  dom ( A u. B ) = { z | E. x z ( A u. B ) x }
16 11 14 15 3eqtr4ri 
 |-  dom ( A u. B ) = ( dom A u. dom B )