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 | ⊢ ( 𝜑 → 𝑅 Er 𝑋 ) | |
| erref.2 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 ) | ||
| Assertion | erref | ⊢ ( 𝜑 → 𝐴 𝑅 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ersymb.1 | ⊢ ( 𝜑 → 𝑅 Er 𝑋 ) | |
| 2 | erref.2 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 ) | |
| 3 | erdm | ⊢ ( 𝑅 Er 𝑋 → dom 𝑅 = 𝑋 ) | |
| 4 | 1 3 | syl | ⊢ ( 𝜑 → dom 𝑅 = 𝑋 ) |
| 5 | 2 4 | eleqtrrd | ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 ) |
| 6 | eldmg | ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) ) | |
| 7 | 2 6 | syl | ⊢ ( 𝜑 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) ) |
| 8 | 5 7 | mpbid | ⊢ ( 𝜑 → ∃ 𝑥 𝐴 𝑅 𝑥 ) |
| 9 | 1 | adantr | ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝑥 ) → 𝑅 Er 𝑋 ) |
| 10 | simpr | ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝑥 ) → 𝐴 𝑅 𝑥 ) | |
| 11 | 9 10 10 | ertr4d | ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝑥 ) → 𝐴 𝑅 𝐴 ) |
| 12 | 8 11 | exlimddv | ⊢ ( 𝜑 → 𝐴 𝑅 𝐴 ) |