Theorem isfld 20071

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2105  CRingccrg 19851  DivRingcdr 20062  Fieldcfield 20063

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3903  df-field 20065

This theorem is referenced by:  fldpropd  20090  primefld  20144  rng1nfld  20620  fldidom  20647  fldidomOLD  20648  fiidomfld  20651  refld  20895  recrng  20897  frlmphllem  21058  frlmphl  21059  recvs  24380  rrxcph  24627  rrx0  24632  ply1pid  25415  lgseisenlem3  26596  lgseisenlem4  26597  ofldlt1  31620  ofldchr  31621  subofld  31623  isarchiofld  31624  reofld  31648  rearchi  31650  srafldlvec  31782  rgmoddim  31799  ccfldextrr  31829  fldextsralvec  31836  extdgcl  31837  extdggt0  31838  fldextid  31840  extdgmul  31842  extdg1id  31844  ccfldsrarelvec  31847  qqhrhm  32045  matunitlindflem1  35833  matunitlindflem2  35834  matunitlindf  35835  fldhmf1  40310  fldcrngd  40465  prjcrv0  40680  fldcat  45899  fldcatALTV  45917