Theorem isfld 20762

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  CRingccrg 20261  DivRingcdr 20751  Fieldcfield 20752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-field 20754

This theorem is referenced by:  flddrngd  20763  fldcrngd  20764  fldpropd  20792  fldidom  20793  fldidomOLD  20794  fiidomfld  20797  rng1nfld  20802  fldcat  20806  fldsdrgfld  20821  primefld  20828  refld  21660  frlmphllem  21823  frlmphl  21824  recvs  25198  rrxcph  25445  rrx0  25450  ply1pid  26242  lgseisenlem3  27439  lgseisenlem4  27440  fracfld  33275  fldgenfld  33287  ofldlt1  33308  ofldchr  33309  subofld  33311  isarchiofld  33312  cnfldfld  33336  reofld  33337  rearchi  33339  qsfld  33491  srafldlvec  33601  rgmoddimOLD  33623  assafld  33650  ccfldextrr  33661  fldextsralvec  33668  extdgcl  33669  extdggt0  33670  fldextid  33672  extdgid  33673  extdgmul  33674  extdg1id  33676  ccfldsrarelvec  33681  2sqr3minply  33738  qqhrhm  33935  matunitlindflem1  37576  matunitlindflem2  37577  matunitlindf  37578  fldhmf1  42047  aks6d1c1p2  42066  aks6d1c2lem4  42084  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks6d1c6lem1  42127  ricfld  42485  fldcatALTV  48054