Theorem isfld 20756

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2105  CRingccrg 20251  DivRingcdr 20745  Fieldcfield 20746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-field 20748

This theorem is referenced by:  flddrngd  20757  fldcrngd  20758  fldpropd  20786  fldidom  20787  fldidomOLD  20788  fiidomfld  20791  rng1nfld  20796  fldcat  20800  fldsdrgfld  20815  primefld  20822  refld  21654  frlmphllem  21817  frlmphl  21818  recvs  25192  rrxcph  25439  rrx0  25444  ply1pid  26236  lgseisenlem3  27435  lgseisenlem4  27436  fracfld  33289  fldgenfld  33301  ofldlt1  33322  ofldchr  33323  subofld  33325  isarchiofld  33326  cnfldfld  33350  reofld  33351  rearchi  33353  qsfld  33505  srafldlvec  33615  rgmoddimOLD  33637  assafld  33664  ccfldextrr  33675  fldextsralvec  33682  extdgcl  33683  extdggt0  33684  fldextid  33686  extdgid  33687  extdgmul  33688  extdg1id  33690  ccfldsrarelvec  33695  2sqr3minply  33752  qqhrhm  33951  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  fldhmf1  42071  aks6d1c1p2  42090  aks6d1c2lem4  42108  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c6lem1  42151  ricfld  42516  fldcatALTV  48174