Theorem subgss 19065

Description: A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.)

Hypothesis

Ref	Expression
issubg.b	⊢ 𝐵 = (Base‘𝐺)

Assertion

Ref	Expression
subgss	⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)

Proof of Theorem subgss

Step	Hyp	Ref	Expression
1		issubg.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
2	1	issubg 19064	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
3	2	simp2bi 1146	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ⊆ wss 3922  ‘cfv 6519  (class class class)co 7394  Basecbs 17185   ↾_s cress 17206  Grpcgrp 18871  SubGrpcsubg 19058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5259  ax-nul 5269  ax-pow 5328  ax-pr 5395

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2880  df-ne 2928  df-ral 3047  df-rex 3056  df-rab 3412  df-v 3457  df-dif 3925  df-un 3927  df-in 3929  df-ss 3939  df-nul 4305  df-if 4497  df-pw 4573  df-sn 4598  df-pr 4600  df-op 4604  df-uni 4880  df-br 5116  df-opab 5178  df-mpt 5197  df-id 5541  df-xp 5652  df-rel 5653  df-cnv 5654  df-co 5655  df-dm 5656  df-rn 5657  df-res 5658  df-ima 5659  df-iota 6472  df-fun 6521  df-fv 6527  df-ov 7397  df-subg 19061

This theorem is referenced by:  subgbas  19068  subg0  19070  subginv  19071  subgsubcl  19075  subgsub  19076  subgmulgcl  19077  subgmulg  19078  issubg2  19079  issubg4  19083  subsubg  19087  subgint  19088  trivsubgd  19091  nsgconj  19097  nsgacs  19100  ssnmz  19104  eqger  19116  eqgid  19118  eqgen  19119  eqgcpbl  19120  lagsubg2  19132  lagsubg  19133  eqg0subg  19134  resghm  19170  ghmnsgima  19178  conjsubg  19188  conjsubgen  19189  conjnmz  19190  conjnmzb  19191  gicsubgen  19217  ghmqusnsglem1  19218  ghmquskerlem1  19221  subgga  19238  gasubg  19240  gastacos  19248  orbstafun  19249  cntrsubgnsg  19281  oddvds2  19502  subgpgp  19533  odcau  19540  pgpssslw  19550  sylow2blem1  19556  sylow2blem2  19557  sylow2blem3  19558  slwhash  19560  fislw  19561  sylow2  19562  sylow3lem1  19563  sylow3lem2  19564  sylow3lem3  19565  sylow3lem4  19566  sylow3lem5  19567  sylow3lem6  19568  lsmval  19584  lsmelval  19585  lsmelvali  19586  lsmelvalm  19587  lsmsubg  19590  lsmub1  19593  lsmub2  19594  lsmless1  19596  lsmless2  19597  lsmless12  19598  lsmass  19605  subglsm  19609  lsmmod  19611  cntzrecd  19614  lsmcntz  19615  lsmcntzr  19616  lsmdisj2  19618  subgdisj1  19627  pj1f  19633  pj1id  19635  pj1lid  19637  pj1rid  19638  pj1ghm  19639  qusecsub  19771  subgabl  19772  ablcntzd  19793  lsmcom  19794  dprdff  19950  dprdfadd  19958  dprdres  19966  dprdss  19967  subgdmdprd  19972  dprdcntz2  19976  dmdprdsplit2lem  19983  ablfacrp  20004  ablfac1eu  20011  pgpfac1lem1  20012  pgpfac1lem2  20013  pgpfac1lem3a  20014  pgpfac1lem3  20015  pgpfac1lem4  20016  pgpfac1lem5  20017  pgpfaclem1  20019  pgpfaclem2  20020  pgpfaclem3  20021  ablfaclem3  20025  ablfac2  20027  prmgrpsimpgd  20052  issubrng2  20473  issubrg2  20507  issubrg3  20515  islss4  20874  dflidl2rng  21134  phssip  21573  mpllsslem  21915  subgtgp  23998  subgntr  24000  opnsubg  24001  clssubg  24002  clsnsg  24003  cldsubg  24004  qustgpopn  24013  qustgphaus  24016  tgptsmscls  24043  subgnm  24527  subgngp  24529  lssnlm  24595  cmscsscms  25280  efgh  26457  efabl  26466  efsubm  26467  subgmulgcld  32992  gsumsubg  32994  qusker  33328  eqgvscpbl  33329  grplsmid  33383  quslsm  33384  qusima  33387  nsgmgc  33391  nsgqusf1olem1  33392  nsgqusf1olem2  33393  nsgqusf1olem3  33394  qsnzr  33434  opprqusplusg  33468  opprqus0g  33469  algextdeglem1  33715  algextdeglem2  33716  algextdeglem3  33717  algextdeglem4  33718  algextdeglem5  33719  nelsubgcld  42457  nelsubgsubcld  42458  idomsubgmo  43154