Theorem unidmrn

Description: The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008)

	Ref	Expression
Assertion	unidmrn	|- U. U. `' A = ( dom A u. ran A )

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' A
2		relfld	|- ( Rel `' A -> U. U. `' A = ( dom `' A u. ran `' A ) )
3	1 2	ax-mp	|- U. U. `' A = ( dom `' A u. ran `' A )
4	3	equncomi	|- U. U. `' A = ( ran `' A u. dom `' A )
5		dfdm4	|- dom A = ran `' A
6		df-rn	|- ran A = dom `' A
7	5 6	uneq12i	|- ( dom A u. ran A ) = ( ran `' A u. dom `' A )
8	4 7	eqtr4i	|- U. U. `' A = ( dom A u. ran A )