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 4168	1 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3923  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  refld  21534  frlmphllem  21695  frlmphl  21696  recvs  25052  rrxcph  25298  rrx0  25303  ply1pid  26094  lgseisenlem3  27294  lgseisenlem4  27295  qfld  33253  fracfld  33264  fldgenfld  33276  ofldlt1  33297  ofldchr  33298  subofld  33300  isarchiofld  33301  cnfldfld  33320  reofld  33321  rearchi  33323  qsfld  33475  srafldlvec  33588  rgmoddimOLD  33612  assafld  33639  ccfldextrr  33648  fldextsralvec  33657  extdgcl  33658  extdggt0  33659  fldextid  33661  extdgid  33662  extdgmul  33665  extdg1id  33667  ccfldsrarelvec  33672  2sqr3minply  33776  qqhrhm  33985  matunitlindflem1  37605  matunitlindflem2  37606  matunitlindf  37607  fldhmf1  42073  aks6d1c1p2  42092  aks6d1c2lem4  42110  aks6d1c5lem3  42120  aks6d1c5lem2  42121  aks6d1c6lem1  42153  ricfld  42511  fldcatALTV  48309