![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isfld | Structured version Visualization version GIF version |
Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.) |
Ref | Expression |
---|---|
isfld | ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-field 18960 | . 2 ⊢ Field = (DivRing ∩ CRing) | |
2 | 1 | elin2 3952 | 1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 ∈ wcel 2145 CRingccrg 18756 DivRingcdr 18957 Fieldcfield 18958 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-in 3730 df-field 18960 |
This theorem is referenced by: fldpropd 18985 rng1nfld 19493 fldidom 19520 fiidomfld 19523 refld 20182 recrng 20184 frlmphllem 20336 frlmphl 20337 rrxcph 23399 ply1pid 24159 lgseisenlem3 25323 lgseisenlem4 25324 ofldlt1 30153 ofldchr 30154 subofld 30156 isarchiofld 30157 reofld 30180 rearchi 30182 qqhrhm 30373 matunitlindflem1 33737 matunitlindflem2 33738 matunitlindf 33739 fldcat 42605 fldcatALTV 42623 |
Copyright terms: Public domain | W3C validator |