Theorem isfld 20671

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  CRingccrg 20167  DivRingcdr 20660  Fieldcfield 20661

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-field 20663

This theorem is referenced by:  flddrngd  20672  fldcrngd  20673  fldpropd  20701  fldidom  20702  fiidomfld  20705  rng1nfld  20710  fldcat  20714  fldsdrgfld  20729  primefld  20736  ofldlt1  20806  subofld  20808  ofldchr  21529  refld  21572  frlmphllem  21733  frlmphl  21734  recvs  25100  rrxcph  25346  rrx0  25351  ply1pid  26142  lgseisenlem3  27342  lgseisenlem4  27343  isarchiofld  33230  qfld  33328  fracfld  33339  fldgenfld  33351  cnfldfld  33372  reofld  33373  rearchi  33376  qsfld  33528  srafldlvec  33691  rgmoddimOLD  33716  assafld  33743  ccfldextrr  33752  fldextsralvec  33761  extdgcl  33762  extdggt0  33763  fldextid  33765  extdgid  33766  extdgmul  33769  extdg1id  33772  ccfldsrarelvec  33777  2sqr3minply  33886  qqhrhm  34095  matunitlindflem1  37756  matunitlindflem2  37757  matunitlindf  37758  fldhmf1  42283  aks6d1c1p2  42302  aks6d1c2lem4  42320  aks6d1c5lem3  42330  aks6d1c5lem2  42331  aks6d1c6lem1  42363  ricfld  42727  fldcatALTV  48519