Metamath Proof Explorer

Theorem relresfld

Description: Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012) (Proof shortened by Eric Schmidt, 16-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 relfld 
 |-  ( Rel R -> U. U. R = ( dom R u. ran R ) )
2 1 reseq2d 
 |-  ( Rel R -> ( R |` U. U. R ) = ( R |` ( dom R u. ran R ) ) )
3 ssun1 
 |-  dom R C_ ( dom R u. ran R )
4 relssres 
 |-  ( ( Rel R /\ dom R C_ ( dom R u. ran R ) ) -> ( R |` ( dom R u. ran R ) ) = R )
5 3 4 mpan2 
 |-  ( Rel R -> ( R |` ( dom R u. ran R ) ) = R )
6 2 5 eqtrd 
 |-  ( Rel R -> ( R |` U. U. R ) = R )