Theorem isfld 19513

Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)

Assertion

Ref	Expression
isfld	⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

Proof of Theorem isfld

Step	Hyp	Ref	Expression
1		df-field 19507	. 2 ⊢ Field = (DivRing ∩ CRing)
2	1	elin2 4176	1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  CRingccrg 19300  DivRingcdr 19504  Fieldcfield 19505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-field 19507

This theorem is referenced by:  fldpropd  19532  primefld  19586  rng1nfld  20053  fldidom  20080  fiidomfld  20083  refld  20765  recrng  20767  frlmphllem  20926  frlmphl  20927  rrxcph  23997  rrx0  24002  ply1pid  24775  lgseisenlem3  25955  lgseisenlem4  25956  ofldlt1  30888  ofldchr  30889  subofld  30891  isarchiofld  30892  reofld  30915  rearchi  30917  srafldlvec  30993  rgmoddim  31010  ccfldextrr  31040  fldextsralvec  31047  extdgcl  31048  extdggt0  31049  fldextid  31051  extdgmul  31053  extdg1id  31055  ccfldsrarelvec  31058  qqhrhm  31232  matunitlindflem1  34890  matunitlindflem2  34891  matunitlindf  34892  fldcat  44360  fldcatALTV  44378