Metamath Proof Explorer

Theorem erssxp

Description: An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion erssxp 
|- ( R Er A -> R C_ ( A X. A ) )

Proof

Step Hyp Ref Expression
1 errel 
 |-  ( R Er A -> Rel R )
2 relssdmrn 
 |-  ( Rel R -> R C_ ( dom R X. ran R ) )
3 1 2 syl 
 |-  ( R Er A -> R C_ ( dom R X. ran R ) )
4 erdm 
 |-  ( R Er A -> dom R = A )
5 errn 
 |-  ( R Er A -> ran R = A )
6 4 5 xpeq12d 
 |-  ( R Er A -> ( dom R X. ran R ) = ( A X. A ) )
7 3 6 sseqtrd 
 |-  ( R Er A -> R C_ ( A X. A ) )