Theorem dfdm2

Description: Alternate definition of domain df-dm that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010)

	Ref	Expression
Assertion	dfdm2	|- dom A = U. U. ( `' A o. A )

Proof

Step	Hyp	Ref	Expression
1		cnvco	|- `' ( `' A o. A ) = ( `' A o. `' `' A )
2		cocnvcnv2	|- ( `' A o. `' `' A ) = ( `' A o. A )
3	1 2	eqtri	|- `' ( `' A o. A ) = ( `' A o. A )
4	3	unieqi	|- U. `' ( `' A o. A ) = U. ( `' A o. A )
5	4	unieqi	|- U. U. `' ( `' A o. A ) = U. U. ( `' A o. A )
6		unidmrn	|- U. U. `' ( `' A o. A ) = ( dom ( `' A o. A ) u. ran ( `' A o. A ) )
7	5 6	eqtr3i	|- U. U. ( `' A o. A ) = ( dom ( `' A o. A ) u. ran ( `' A o. A ) )
8		df-rn	|- ran A = dom `' A
9	8	eqcomi	|- dom `' A = ran A
10		dmcoeq	|- ( dom `' A = ran A -> dom ( `' A o. A ) = dom A )
11	9 10	ax-mp	|- dom ( `' A o. A ) = dom A
12		rncoeq	|- ( dom `' A = ran A -> ran ( `' A o. A ) = ran `' A )
13	9 12	ax-mp	|- ran ( `' A o. A ) = ran `' A
14		dfdm4	|- dom A = ran `' A
15	13 14	eqtr4i	|- ran ( `' A o. A ) = dom A
16	11 15	uneq12i	|- ( dom ( `' A o. A ) u. ran ( `' A o. A ) ) = ( dom A u. dom A )
17		unidm	|- ( dom A u. dom A ) = dom A
18	7 16 17	3eqtrri	|- dom A = U. U. ( `' A o. A )