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		dmcocnv1	|- dom ( `' A o. A ) = dom A
9		rncocnv1	|- ran ( `' A o. A ) = dom A
10	8 9	uneq12i	|- ( dom ( `' A o. A ) u. ran ( `' A o. A ) ) = ( dom A u. dom A )
11		unidm	|- ( dom A u. dom A ) = dom A
12	7 10 11	3eqtrri	|- dom A = U. U. ( `' A o. A )