Theorem grpbn0 19056

Description: The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)

Hypothesis

Ref	Expression
grpbn0.b	⊢ 𝐵 = (Base‘𝐺)

Assertion

Ref	Expression
grpbn0	⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)

Proof of Theorem grpbn0

Step	Hyp	Ref	Expression
1		grpbn0.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
2		eqid 2765	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
3	1, 2	grpidcl 19055	. 2 ⊢ (𝐺 ∈ Grp → (0g‘𝐺) ∈ 𝐵)
4	3	ne0d 4295	1 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∅c0 4286  ‘cfv 6540  Basecbs 17286  0_gc0g 17509  Grpcgrp 19023

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-riota 7373  df-ov 7419  df-0g 17511  df-mgm 18715  df-sgrp 18798  df-mnd 18814  df-grp 19026

This theorem is used by:  grpn0  19061  dfgrp3  19128  issubg2  19231  grpissubg  19236  qustriv  19275  ghmrn  19322  gexcl3  19680  gexcl2  19682  sylow1lem1  19691  sylow1lem3  19693  sylow1lem5  19695  pgpfi  19698  pgpfi2  19699  sylow2blem3  19715  slwhash  19717  fislw  19718  gexex  19946  lt6abl  19988  ablfac1lem  20163  ablfac1b  20165  ablfac1c  20166  ablfac1eu  20168  pgpfac1lem2  20170  pgpfac1lem3a  20171  ablfaclem3  20182  dvdsr02  20479  0ringnnzr  20652  lmodbn0  21021  lmodsn0  21024  rmodislmodlem  21079  rmodislmod  21080  islss3  21109  rnglidl1  21387  isclmp  25285  dfacbasgrp  43868