Theorem isfld 20712

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  CRingccrg 20206  DivRingcdr 20701  Fieldcfield 20702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-field 20704

This theorem is referenced by:  flddrngd  20713  fldcrngd  20714  fldpropd  20742  fldidom  20743  fiidomfld  20746  rng1nfld  20751  fldcat  20755  fldsdrgfld  20770  primefld  20777  ofldlt1  20847  subofld  20849  ofldchr  21551  refld  21594  frlmphllem  21755  frlmphl  21756  recvs  25131  rrxcph  25377  rrx0  25382  ply1pid  26166  lgseisenlem3  27358  lgseisenlem4  27359  isarchiofld  33280  qfld  33381  fracfld  33392  fldgenfld  33404  cnfldfld  33425  reofld  33426  rearchi  33429  qsfld  33581  srafldlvec  33770  assafld  33821  ccfldextrr  33830  fldextsralvec  33839  extdgcl  33840  extdggt0  33841  fldextid  33843  extdgid  33844  extdgmul  33847  extdg1id  33850  ccfldsrarelvec  33855  2sqr3minply  33964  qqhrhm  34173  matunitlindflem1  37983  matunitlindflem2  37984  matunitlindf  37985  fldhmf1  42575  aks6d1c1p2  42594  aks6d1c2lem4  42612  aks6d1c5lem3  42622  aks6d1c5lem2  42623  aks6d1c6lem1  42655  ricfld  43016  fldcatALTV  48822