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	|- ( ph -> R Er X )
	erref.2	|- ( ph -> A e. X )
Assertion	erref	|- ( ph -> A R A )

Proof

Step	Hyp	Ref	Expression
1		ersymb.1	|- ( ph -> R Er X )
2		erref.2	|- ( ph -> A e. X )
3		erdm	|- ( R Er X -> dom R = X )
4	1 3	syl	|- ( ph -> dom R = X )
5	2 4	eleqtrrd	|- ( ph -> A e. dom R )
6		eldmg	|- ( A e. X -> ( A e. dom R <-> E. x A R x ) )
7	2 6	syl	|- ( ph -> ( A e. dom R <-> E. x A R x ) )
8	5 7	mpbid	|- ( ph -> E. x A R x )
9	1	adantr	|- ( ( ph /\ A R x ) -> R Er X )
10		simpr	|- ( ( ph /\ A R x ) -> A R x )
11	9 10 10	ertr4d	|- ( ( ph /\ A R x ) -> A R A )
12	8 11	exlimddv	|- ( ph -> A R A )