Theorem isfld 20655

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2111  CRingccrg 20152  DivRingcdr 20644  Fieldcfield 20645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-field 20647

This theorem is referenced by:  flddrngd  20656  fldcrngd  20657  fldpropd  20685  fldidom  20686  fiidomfld  20689  rng1nfld  20694  fldcat  20698  fldsdrgfld  20713  primefld  20720  ofldlt1  20790  subofld  20792  ofldchr  21513  refld  21556  frlmphllem  21717  frlmphl  21718  recvs  25073  rrxcph  25319  rrx0  25324  ply1pid  26115  lgseisenlem3  27315  lgseisenlem4  27316  isarchiofld  33168  qfld  33263  fracfld  33274  fldgenfld  33286  cnfldfld  33307  reofld  33308  rearchi  33311  qsfld  33463  srafldlvec  33598  rgmoddimOLD  33623  assafld  33650  ccfldextrr  33659  fldextsralvec  33668  extdgcl  33669  extdggt0  33670  fldextid  33672  extdgid  33673  extdgmul  33676  extdg1id  33679  ccfldsrarelvec  33684  2sqr3minply  33793  qqhrhm  34002  matunitlindflem1  37666  matunitlindflem2  37667  matunitlindf  37668  fldhmf1  42193  aks6d1c1p2  42212  aks6d1c2lem4  42230  aks6d1c5lem3  42240  aks6d1c5lem2  42241  aks6d1c6lem1  42273  ricfld  42633  fldcatALTV  48441