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 8391 | . 2 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) | |
2 | 1 | simp2bi 1148 | 1 ⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∪ cun 3864 ⊆ wss 3866 ◡ccnv 5550 dom cdm 5551 ∘ ccom 5555 Rel wrel 5556 Er wer 8388 |
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 210 df-an 400 df-3an 1091 df-er 8391 |
This theorem is referenced by: ercl 8402 erref 8411 errn 8413 erssxp 8414 erexb 8416 ereldm 8439 uniqs2 8461 iiner 8471 eceqoveq 8504 prsrlem1 10686 ltsrpr 10691 0nsr 10693 divsfval 17052 sylow1lem3 18989 sylow1lem5 18991 sylow2a 19008 vitalilem2 24506 vitalilem3 24507 vitalilem5 24509 |
Copyright terms: Public domain | W3C validator |