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 ( 𝑅 Er 𝐴𝑅 ⊆ ( 𝐴 × 𝐴 ) )

Proof

Step Hyp Ref Expression
1 errel ( 𝑅 Er 𝐴 → Rel 𝑅 )
2 relssdmrn ( Rel 𝑅𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
3 1 2 syl ( 𝑅 Er 𝐴𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
4 erdm ( 𝑅 Er 𝐴 → dom 𝑅 = 𝐴 )
5 errn ( 𝑅 Er 𝐴 → ran 𝑅 = 𝐴 )
6 4 5 xpeq12d ( 𝑅 Er 𝐴 → ( dom 𝑅 × ran 𝑅 ) = ( 𝐴 × 𝐴 ) )
7 3 6 sseqtrd ( 𝑅 Er 𝐴𝑅 ⊆ ( 𝐴 × 𝐴 ) )