Theorem grpbn0 18933

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274  ‘cfv 6492  Basecbs 17170  0_gc0g 17393  Grpcgrp 18900

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-riota 7317  df-ov 7363  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903

This theorem is referenced by:  grpn0  18938  dfgrp3  19006  issubg2  19108  grpissubg  19113  ghmrn  19195  gexcl3  19553  gexcl2  19555  sylow1lem1  19564  sylow1lem3  19566  sylow1lem5  19568  pgpfi  19571  pgpfi2  19572  sylow2blem3  19588  slwhash  19590  fislw  19591  gexex  19819  lt6abl  19861  ablfac1lem  20036  ablfac1b  20038  ablfac1c  20039  ablfac1eu  20041  pgpfac1lem2  20043  pgpfac1lem3a  20044  ablfaclem3  20055  dvdsr02  20343  0ringnnzr  20493  lmodbn0  20857  lmodsn0  20860  rmodislmodlem  20915  rmodislmod  20916  islss3  20945  rnglidl1  21222  isclmp  25074  qustriv  33439  dfacbasgrp  43554