Theorem isfld 20717

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  CRingccrg 20215  DivRingcdr 20706  Fieldcfield 20707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-field 20709

This theorem is referenced by:  flddrngd  20718  fldcrngd  20719  fldpropd  20747  fldidom  20748  fiidomfld  20751  rng1nfld  20756  fldcat  20760  fldsdrgfld  20775  primefld  20782  ofldlt1  20852  subofld  20854  ofldchr  21556  refld  21599  frlmphllem  21760  frlmphl  21761  recvs  25113  rrxcph  25359  rrx0  25364  ply1pid  26148  lgseisenlem3  27340  lgseisenlem4  27341  isarchiofld  33260  qfld  33358  fracfld  33369  fldgenfld  33381  cnfldfld  33402  reofld  33403  rearchi  33406  qsfld  33558  srafldlvec  33730  assafld  33781  ccfldextrr  33790  fldextsralvec  33799  extdgcl  33800  extdggt0  33801  fldextid  33803  extdgid  33804  extdgmul  33807  extdg1id  33810  ccfldsrarelvec  33815  2sqr3minply  33924  qqhrhm  34133  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  fldhmf1  42529  aks6d1c1p2  42548  aks6d1c2lem4  42566  aks6d1c5lem3  42576  aks6d1c5lem2  42577  aks6d1c6lem1  42609  ricfld  42975  fldcatALTV  48807