Theorem isfld 20625

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  CRingccrg 20119  DivRingcdr 20614  Fieldcfield 20615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-field 20617

This theorem is referenced by:  flddrngd  20626  fldcrngd  20627  fldpropd  20655  fldidom  20656  fiidomfld  20659  rng1nfld  20664  fldcat  20668  fldsdrgfld  20683  primefld  20690  refld  21504  frlmphllem  21665  frlmphl  21666  recvs  25022  rrxcph  25268  rrx0  25273  ply1pid  26064  lgseisenlem3  27264  lgseisenlem4  27265  qfld  33220  fracfld  33231  fldgenfld  33243  ofldlt1  33264  ofldchr  33265  subofld  33267  isarchiofld  33268  cnfldfld  33287  reofld  33288  rearchi  33290  qsfld  33442  srafldlvec  33555  rgmoddimOLD  33579  assafld  33606  ccfldextrr  33615  fldextsralvec  33624  extdgcl  33625  extdggt0  33626  fldextid  33628  extdgid  33629  extdgmul  33632  extdg1id  33634  ccfldsrarelvec  33639  2sqr3minply  33743  qqhrhm  33952  matunitlindflem1  37583  matunitlindflem2  37584  matunitlindf  37585  fldhmf1  42051  aks6d1c1p2  42070  aks6d1c2lem4  42088  aks6d1c5lem3  42098  aks6d1c5lem2  42099  aks6d1c6lem1  42131  ricfld  42491  fldcatALTV  48292