Theorem grpbn0 19227

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∅c0 4281  ‘cfv 6566  Basecbs 17431  0_gc0g 17660  Grpcgrp 19194

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574  df-riota 7408  df-ov 7454  df-0g 17662  df-mgm 18866  df-sgrp 18958  df-mnd 18974  df-grp 19197

This theorem is used by:  grpn0  19232  dfgrp3  19299  issubg2  19402  grpissubg  19407  qustriv  19446  ghmrn  19493  gexcl3  19852  gexcl2  19854  sylow1lem1  19863  sylow1lem3  19865  sylow1lem5  19867  pgpfi  19870  pgpfi2  19871  sylow2blem3  19887  slwhash  19889  fislw  19890  gexex  20118  lt6abl  20160  ablfac1lem  20335  ablfac1b  20337  ablfac1c  20338  ablfac1eu  20340  pgpfac1lem2  20342  pgpfac1lem3a  20343  ablfaclem3  20354  ringbn0  20519  dvdsr02  20653  0ringnnzr  20827  lmodbn0  21197  lmodsn0  21200  rmodislmodlem  21255  rmodislmod  21256  islss3  21285  rnglidl1  21563  isclmp  25473  dfacbasgrp  44375