Metamath Proof Explorer

Theorem relcnvfld

Description: if R is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009)

Ref Expression
Assertion relcnvfld 
|- ( Rel R -> U. U. R = U. U. `' R )

Proof

Step Hyp Ref Expression
1 relfld 
 |-  ( Rel R -> U. U. R = ( dom R u. ran R ) )
2 unidmrn 
 |-  U. U. `' R = ( dom R u. ran R )
3 1 2 eqtr4di 
 |-  ( Rel R -> U. U. R = U. U. `' R )