Theorem grpbn0 18940

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ≠ wne 2935  ∅c0 4268  ‘cfv 6492  Basecbs 17177  0_gc0g 17400  Grpcgrp 18907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-riota 7320  df-ov 7366  df-0g 17402  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-grp 18910

This theorem is referenced by:  grpn0  18945  dfgrp3  19013  issubg2  19115  grpissubg  19120  ghmrn  19202  gexcl3  19560  gexcl2  19562  sylow1lem1  19571  sylow1lem3  19573  sylow1lem5  19575  pgpfi  19578  pgpfi2  19579  sylow2blem3  19595  slwhash  19597  fislw  19598  gexex  19826  lt6abl  19868  ablfac1lem  20043  ablfac1b  20045  ablfac1c  20046  ablfac1eu  20048  pgpfac1lem2  20050  pgpfac1lem3a  20051  ablfaclem3  20062  dvdsr02  20350  0ringnnzr  20504  lmodbn0  20868  lmodsn0  20871  rmodislmodlem  20926  rmodislmod  20927  islss3  20956  rnglidl1  21232  isclmp  25089  qustriv  33454  dfacbasgrp  43560