| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > erdm | Structured version Visualization version GIF version | ||
| Description: The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) |
| Ref | Expression |
|---|---|
| erdm | ⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-er 8745 | . 2 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) | |
| 2 | 1 | simp2bi 1147 | 1 ⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∪ cun 3949 ⊆ wss 3951 ◡ccnv 5684 dom cdm 5685 ∘ ccom 5689 Rel wrel 5690 Er wer 8742 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-er 8745 |
| This theorem is referenced by: ercl 8756 erref 8765 errn 8767 erssxp 8768 erexb 8770 ereldm 8795 uniqs2 8819 iiner 8829 eceqoveq 8862 prsrlem1 11112 ltsrpr 11117 0nsr 11119 divsfval 17592 sylow1lem3 19618 sylow1lem5 19620 sylow2a 19637 vitalilem2 25644 vitalilem3 25645 vitalilem5 25647 prjspnn0 42632 |
| Copyright terms: Public domain | W3C validator |