This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 𝑅 𝐴 )