Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > erdm | Structured version Visualization version Unicode version |
Description: The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) |
Ref | Expression |
---|---|
erdm |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-er 7742 | . 2 | |
2 | 1 | simp2bi 1077 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cun 3572 wss 3574 ccnv 5113 cdm 5114 ccom 5118 wrel 5119 wer 7739 |
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 197 df-an 386 df-3an 1039 df-er 7742 |
This theorem is referenced by: ercl 7753 erref 7762 errn 7764 erssxp 7765 erexb 7767 ereldm 7790 uniqs2 7809 iiner 7819 eceqoveq 7853 prsrlem1 9893 ltsrpr 9898 0nsr 9900 divsfval 16207 sylow1lem3 18015 sylow1lem5 18017 sylow2a 18034 vitalilem2 23378 vitalilem3 23379 vitalilem5 23381 |
Copyright terms: Public domain | W3C validator |