# Metamath Proof Explorer

## 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 {A}{R}{A}$

### 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}↔\exists {x}\phantom{\rule{.4em}{0ex}}{A}{R}{x}\right)$
7 2 6 syl ${⊢}{\phi }\to \left({A}\in \mathrm{dom}{R}↔\exists {x}\phantom{\rule{.4em}{0ex}}{A}{R}{x}\right)$
8 5 7 mpbid ${⊢}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{A}{R}{x}$
9 1 adantr ${⊢}\left({\phi }\wedge {A}{R}{x}\right)\to {R}\mathrm{Er}{X}$
10 simpr ${⊢}\left({\phi }\wedge {A}{R}{x}\right)\to {A}{R}{x}$
11 9 10 10 ertr4d ${⊢}\left({\phi }\wedge {A}{R}{x}\right)\to {A}{R}{A}$
12 8 11 exlimddv ${⊢}{\phi }\to {A}{R}{A}$