Theorem erref

Description: An equivalence relation is reflexive on its field. Compare Theorem 3M of Enderton p. 56. (Contributed by Mario Carneiro, 6-May-2013) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	ersymb.1	$$⊢\phi \to R\mathrm{Er}X$$
	erref.2	$$⊢\phi \to A\in X$$
Assertion	erref	$$⊢\phi \to ARA$$

Proof

Step	Hyp	Ref	Expression
1		ersymb.1	$$⊢\phi \to R\mathrm{Er}X$$
2		erref.2	$$⊢\phi \to A\in X$$
3		erdm	$$⊢R\mathrm{Er}X\to \mathrm{dom}R=X$$
4	1 3	syl	$$⊢\phi \to \mathrm{dom}R=X$$
5	2 4	eleqtrrd	$$⊢\phi \to A\in \mathrm{dom}R$$
6		eldmg	$$⊢A\in X\to \left(A\in \mathrm{dom}R\leftrightarrow \exists xARx\right)$$
7	2 6	syl	$$⊢\phi \to \left(A\in \mathrm{dom}R\leftrightarrow \exists xARx\right)$$
8	5 7	mpbid	$$⊢\phi \to \exists xARx$$
9	1	adantr	$$⊢\left(\phi \wedge ARx\right)\to R\mathrm{Er}X$$
10		simpr	$$⊢\left(\phi \wedge ARx\right)\to ARx$$
11	9 10 10	ertr4d	$$⊢\left(\phi \wedge ARx\right)\to ARA$$
12	8 11	exlimddv	$$⊢\phi \to ARA$$