Theorem isfld 20656

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

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

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 3924  df-field 20648

This theorem is referenced by:  flddrngd  20657  fldcrngd  20658  fldpropd  20686  fldidom  20687  fiidomfld  20690  rng1nfld  20695  fldcat  20699  fldsdrgfld  20714  primefld  20721  refld  21535  frlmphllem  21696  frlmphl  21697  recvs  25053  rrxcph  25299  rrx0  25304  ply1pid  26095  lgseisenlem3  27295  lgseisenlem4  27296  qfld  33254  fracfld  33265  fldgenfld  33277  ofldlt1  33298  ofldchr  33299  subofld  33301  isarchiofld  33302  cnfldfld  33321  reofld  33322  rearchi  33324  qsfld  33476  srafldlvec  33589  rgmoddimOLD  33613  assafld  33640  ccfldextrr  33649  fldextsralvec  33658  extdgcl  33659  extdggt0  33660  fldextid  33662  extdgid  33663  extdgmul  33666  extdg1id  33668  ccfldsrarelvec  33673  2sqr3minply  33777  qqhrhm  33986  matunitlindflem1  37617  matunitlindflem2  37618  matunitlindf  37619  fldhmf1  42085  aks6d1c1p2  42104  aks6d1c2lem4  42122  aks6d1c5lem3  42132  aks6d1c5lem2  42133  aks6d1c6lem1  42165  ricfld  42525  fldcatALTV  48323