Theorem isfld 20700

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  CRingccrg 20194  DivRingcdr 20689  Fieldcfield 20690

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-field 20692

This theorem is referenced by:  flddrngd  20701  fldcrngd  20702  fldpropd  20730  fldidom  20731  fiidomfld  20734  rng1nfld  20739  fldcat  20743  fldsdrgfld  20758  primefld  20765  refld  21579  frlmphllem  21740  frlmphl  21741  recvs  25097  rrxcph  25344  rrx0  25349  ply1pid  26140  lgseisenlem3  27340  lgseisenlem4  27341  qfld  33291  fracfld  33302  fldgenfld  33314  ofldlt1  33335  ofldchr  33336  subofld  33338  isarchiofld  33339  cnfldfld  33358  reofld  33359  rearchi  33361  qsfld  33513  srafldlvec  33626  rgmoddimOLD  33650  assafld  33677  ccfldextrr  33688  fldextsralvec  33697  extdgcl  33698  extdggt0  33699  fldextid  33701  extdgid  33702  extdgmul  33705  extdg1id  33707  ccfldsrarelvec  33712  2sqr3minply  33814  qqhrhm  34020  matunitlindflem1  37640  matunitlindflem2  37641  matunitlindf  37642  fldhmf1  42103  aks6d1c1p2  42122  aks6d1c2lem4  42140  aks6d1c5lem3  42150  aks6d1c5lem2  42151  aks6d1c6lem1  42183  ricfld  42553  fldcatALTV  48306