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 | |- ( ph -> EqvRel R ) |
|
| eqvrelref.2 | |- ( ph -> A e. dom R ) |
||
| Assertion | eqvrelref | |- ( ph -> A R A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqvrelref.1 | |- ( ph -> EqvRel R ) |
|
| 2 | eqvrelref.2 | |- ( ph -> A e. dom R ) |
|
| 3 | eqvrelrel | |- ( EqvRel R -> Rel R ) |
|
| 4 | releldmb | |- ( Rel R -> ( A e. dom R <-> E. x A R x ) ) |
|
| 5 | 1 3 4 | 3syl | |- ( ph -> ( A e. dom R <-> E. x A R x ) ) |
| 6 | 2 5 | mpbid | |- ( ph -> E. x A R x ) |
| 7 | 1 | adantr | |- ( ( ph /\ A R x ) -> EqvRel R ) |
| 8 | simpr | |- ( ( ph /\ A R x ) -> A R x ) |
|
| 9 | 7 8 8 | eqvreltr4d | |- ( ( ph /\ A R x ) -> A R A ) |
| 10 | 6 9 | exlimddv | |- ( ph -> A R A ) |