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	⊢ ( 𝜑 → EqvRel 𝑅 )
	eqvrelref.2	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )
Assertion	eqvrelref	⊢ ( 𝜑 → 𝐴 𝑅 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqvrelref.1	⊢ ( 𝜑 → EqvRel 𝑅 )
2		eqvrelref.2	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )
3		eqvrelrel	⊢ ( EqvRel 𝑅 → Rel 𝑅 )
4		releldmb	⊢ ( Rel 𝑅 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )
5	1 3 4	3syl	⊢ ( 𝜑 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )
6	2 5	mpbid	⊢ ( 𝜑 → ∃ 𝑥 𝐴 𝑅 𝑥 )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝑥 ) → EqvRel 𝑅 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝑥 ) → 𝐴 𝑅 𝑥 )
9	7 8 8	eqvreltr4d	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝑥 ) → 𝐴 𝑅 𝐴 )
10	6 9	exlimddv	⊢ ( 𝜑 → 𝐴 𝑅 𝐴 )