Theorem grpbn0 18793

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 2731	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
3	1, 2	grpidcl 18792	. 2 ⊢ (𝐺 ∈ Grp → (0g‘𝐺) ∈ 𝐵)
4	3	ne0d 4300	1 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ≠ wne 2939  ∅c0 4287  ‘cfv 6501  Basecbs 17094  0_gc0g 17335  Grpcgrp 18762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-riota 7318  df-ov 7365  df-0g 17337  df-mgm 18511  df-sgrp 18560  df-mnd 18571  df-grp 18765

This theorem is referenced by:  grpn0  18796  dfgrp3  18860  issubg2  18957  grpissubg  18962  ghmrn  19035  gexcl3  19383  gexcl2  19385  sylow1lem1  19394  sylow1lem3  19396  sylow1lem5  19398  pgpfi  19401  pgpfi2  19402  sylow2blem3  19418  slwhash  19420  fislw  19421  gexex  19645  lt6abl  19686  ablfac1lem  19861  ablfac1b  19863  ablfac1c  19864  ablfac1eu  19866  pgpfac1lem2  19868  pgpfac1lem3a  19869  ablfaclem3  19880  dvdsr02  20099  0ringnnzr  20212  lmodbn0  20389  lmodsn0  20392  rmodislmodlem  20446  rmodislmod  20447  rmodislmodOLD  20448  islss3  20477  isclmp  24497  qustriv  32224  dfacbasgrp  41493