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		unab	|- ( { y | E. x y A x } u. { y | E. x y B x } ) = { y | ( E. x y A x \/ E. x y B x ) }
2		brun	|- ( y ( A u. B ) x <-> ( y A x \/ y B x ) )
3	2	exbii	|- ( E. x y ( A u. B ) x <-> E. x ( y A x \/ y B x ) )
4		19.43	|- ( E. x ( y A x \/ y B x ) <-> ( E. x y A x \/ E. x y B x ) )
5	3 4	bitr2i	|- ( ( E. x y A x \/ E. x y B x ) <-> E. x y ( A u. B ) x )
6	5	abbii	|- { y | ( E. x y A x \/ E. x y B x ) } = { y | E. x y ( A u. B ) x }
7	1 6	eqtri	|- ( { y | E. x y A x } u. { y | E. x y B x } ) = { y | E. x y ( A u. B ) x }
8		df-dm	|- dom A = { y | E. x y A x }
9		df-dm	|- dom B = { y | E. x y B x }
10	8 9	uneq12i	|- ( dom A u. dom B ) = ( { y | E. x y A x } u. { y | E. x y B x } )
11		df-dm	|- dom ( A u. B ) = { y | E. x y ( A u. B ) x }
12	7 10 11	3eqtr4ri	|- dom ( A u. B ) = ( dom A u. dom B )