Theorem isfld 20368

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 20360	. 2 ⊢ Field = (DivRing ∩ CRing)
2	1	elin2 4198	1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

Syntax hints:   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  CRingccrg 20057  DivRingcdr 20357  Fieldcfield 20358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-field 20360

This theorem is referenced by:  flddrngd  20369  fldcrngd  20370  fldpropd  20395  rng1nfld  20400  fldsdrgfld  20414  primefld  20421  fldidom  20923  fldidomOLD  20924  fiidomfld  20927  refld  21172  frlmphllem  21335  frlmphl  21336  recvs  24662  rrxcph  24909  rrx0  24914  ply1pid  25697  lgseisenlem3  26880  lgseisenlem4  26881  fldgenfld  32410  ofldlt1  32431  ofldchr  32432  subofld  32434  isarchiofld  32435  reofld  32459  rearchi  32461  qsfld  32612  srafldlvec  32676  rgmoddimOLD  32695  ccfldextrr  32727  fldextsralvec  32734  extdgcl  32735  extdggt0  32736  fldextid  32738  extdgid  32739  extdgmul  32740  extdg1id  32742  ccfldsrarelvec  32745  qqhrhm  32969  matunitlindflem1  36484  matunitlindflem2  36485  matunitlindf  36486  fldhmf1  40955  ricfld  41105  fldcat  46980  fldcatALTV  46998