![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isfld | Structured version Visualization version Unicode version |
Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
Ref | Expression |
---|---|
isfld |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-field 18027 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | elin2 3633 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-in 3423 df-field 18027 |
This theorem is referenced by: fldpropd 18052 rng1nfld 18551 fldidom 18578 fiidomfld 18581 refld 19236 recrng 19238 frlmphllem 19387 frlmphl 19388 rrxcph 22400 ply1pid 23186 lgseisenlem3 24328 lgseisenlem4 24329 ofldlt1 28625 ofldchr 28626 subofld 28628 isarchiofld 28629 reofld 28652 rearchi 28654 qqhrhm 28842 fldcat 40357 fldcatALTV 40376 |
Copyright terms: Public domain | W3C validator |