Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dfom3 | Unicode version |
Description: Alias for df-iom 4314. Use it instead of df-iom 4314 for naming consistency with set.mm. (Contributed by NM, 6-Aug-1994.) |
Ref | Expression |
---|---|
dfom3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iom 4314 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 97 wceq 1243 wcel 1393 cab 2026 wral 2306 c0 3224 cint 3615 csuc 4102 com 4313 |
This theorem depends on definitions: df-iom 4314 |
This theorem is referenced by: omex 4316 peano1 4317 peano2 4318 peano5 4321 bj-dfom 10057 |
Copyright terms: Public domain | W3C validator |