Theorem isfld 20823

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  CRingccrg 20315  DivRingcdr 20812  Fieldcfield 20813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-field 20815

This theorem is referenced by:  flddrngd  20824  fldcrngd  20825  fldpropd  20851  fldidom  20852  fiidomfld  20855  rng1nfld  20859  fldcat  20863  fldsdrgfld  20878  primefld  20885  ofldlt1  20955  subofld  20957  ofldchr  21694  refld  21737  frlmphllem  21898  frlmphl  21899  recvs  25273  rrxcph  25519  rrx0  25524  ply1pid  26308  lgseisenlem3  27506  lgseisenlem4  27507  isarchiofld  33459  qfld  33560  fracfld  33571  fldgenfld  33583  cnfldfld  33604  reofld  33605  rearchi  33608  qsfld  33724  srafldlvec  33920  assafld  33971  ccfldextrr  33980  fldextsralvec  33989  extdgcl  33990  extdggt0  33991  fldextid  33993  extdgid  33994  extdgmul  33997  extdg1id  34000  ccfldsrarelvec  34005  2sqr3minply  34114  qqhrhm  34323  matunitlindflem1  38154  matunitlindflem2  38155  matunitlindf  38156  fldhmf1  42746  aks6d1c1p2  42765  aks6d1c2lem4  42783  aks6d1c5lem3  42793  aks6d1c5lem2  42794  aks6d1c6lem1  42826  ricfld  43189  fldcatALTV  48984