MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpbn0 Structured version   Visualization version   GIF version

Theorem grpbn0 18127
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
StepHypRef Expression
1 grpbn0.b . . 3 𝐵 = (Base‘𝐺)
2 eqid 2801 . . 3 (0g𝐺) = (0g𝐺)
31, 2grpidcl 18126 . 2 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝐵)
43ne0d 4254 1 (𝐺 ∈ Grp → 𝐵 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  wne 2990  c0 4246  cfv 6328  Basecbs 16478  0gc0g 16708  Grpcgrp 18098
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-iota 6287  df-fun 6330  df-fv 6336  df-riota 7097  df-ov 7142  df-0g 16710  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-grp 18101
This theorem is referenced by:  grpn0  18130  dfgrp3  18193  issubg2  18289  grpissubg  18294  ghmrn  18366  gexcl3  18707  gexcl2  18709  sylow1lem1  18718  sylow1lem3  18720  sylow1lem5  18722  pgpfi  18725  pgpfi2  18726  sylow2blem3  18742  slwhash  18744  fislw  18745  gexex  18969  lt6abl  19011  ablfac1lem  19186  ablfac1b  19188  ablfac1c  19189  ablfac1eu  19191  pgpfac1lem2  19193  pgpfac1lem3a  19194  ablfaclem3  19205  dvdsr02  19405  lmodbn0  19640  lmodsn0  19643  rmodislmodlem  19697  rmodislmod  19698  islss3  19727  0ringnnzr  20038  isclmp  23705  qustriv  30983  dfacbasgrp  40039
  Copyright terms: Public domain W3C validator