Theorem eqvrelref

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) (Revised by Peter Mazsa, 2-Jun-2019)

	Ref	Expression
Hypotheses	eqvrelref.1	$$⊢\phi \to EqvRelR$$
	eqvrelref.2	$$⊢\phi \to A\in \mathrm{dom}R$$
Assertion	eqvrelref	$$⊢\phi \to ARA$$

Proof

Step	Hyp	Ref	Expression
1		eqvrelref.1	$$⊢\phi \to EqvRelR$$
2		eqvrelref.2	$$⊢\phi \to A\in \mathrm{dom}R$$
3		eqvrelrel	$$⊢EqvRelR\to \mathrm{Rel}R$$
4		releldmb	$$⊢\mathrm{Rel}R\to \left(A\in \mathrm{dom}R\leftrightarrow \exists xARx\right)$$
5	1 3 4	3syl	$$⊢\phi \to \left(A\in \mathrm{dom}R\leftrightarrow \exists xARx\right)$$
6	2 5	mpbid	$$⊢\phi \to \exists xARx$$
7	1	adantr	$$⊢\left(\phi \wedge ARx\right)\to EqvRelR$$
8		simpr	$$⊢\left(\phi \wedge ARx\right)\to ARx$$
9	7 8 8	eqvreltr4d	$$⊢\left(\phi \wedge ARx\right)\to ARA$$
10	6 9	exlimddv	$$⊢\phi \to ARA$$