Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > erdm | 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 6397 | . 2 | |
2 | 1 | simp2bi 982 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 cun 3039 wss 3041 ccnv 4508 cdm 4509 ccom 4513 wrel 4514 wer 6394 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 949 df-er 6397 |
This theorem is referenced by: ercl 6408 erref 6417 errn 6419 erssxp 6420 erexb 6422 ereldm 6440 uniqs2 6457 iinerm 6469 th3qlem1 6499 0nnq 7140 nnnq0lem1 7222 prsrlem1 7518 gt0srpr 7524 0nsr 7525 |
Copyright terms: Public domain | W3C validator |