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