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\mathrm{Er}A\to R\subseteq A\times A$$

Proof

Step	Hyp	Ref	Expression
1		errel	$$⊢R\mathrm{Er}A\to \mathrm{Rel}R$$
2		relssdmrn	$$⊢\mathrm{Rel}R\to R\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
3	1 2	syl	$$⊢R\mathrm{Er}A\to R\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
4		erdm	$$⊢R\mathrm{Er}A\to \mathrm{dom}R=A$$
5		errn	$$⊢R\mathrm{Er}A\to \mathrm{ran}R=A$$
6	4 5	xpeq12d	$$⊢R\mathrm{Er}A\to \mathrm{dom}R\times \mathrm{ran}R=A\times A$$
7	3 6	sseqtrd	$$⊢R\mathrm{Er}A\to R\subseteq A\times A$$