Theorem subgss 19193

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 19192	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
3	2	simp2bi 1162	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   ⊆ wss 3913  ‘cfv 6537  (class class class)co 7411  Basecbs 17269   ↾_s cress 17290  Grpcgrp 19000  SubGrpcsubg 19186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7414  df-subg 19189

This theorem is referenced by:  subgbas  19196  subg0  19198  subginv  19199  subgsubcl  19204  subgsub  19205  subgmulgcl  19206  subgmulg  19207  issubg2  19208  issubg4  19212  subsubg  19216  subgint  19217  trivsubgd  19219  nsgconj  19225  nsgacs  19228  ssnmz  19232  eqger  19246  eqgid  19248  eqgen  19249  eqgcpbl  19250  lagsubg2  19265  lagsubg  19266  eqg0subg  19267  resghm  19302  ghmnsgima  19310  conjsubg  19320  conjsubgen  19321  conjnmz  19322  conjnmzb  19323  gicsubgen  19349  ghmqusnsglem1  19350  ghmquskerlem1  19353  subgga  19370  gasubg  19372  gastacos  19380  orbstafun  19381  cntrsubgnsg  19413  oddvds2  19636  subgpgp  19667  odcau  19674  pgpssslw  19684  sylow2blem1  19690  sylow2blem2  19691  sylow2blem3  19692  slwhash  19694  fislw  19695  sylow2  19696  sylow3lem1  19697  sylow3lem2  19698  sylow3lem3  19699  sylow3lem4  19700  sylow3lem5  19701  sylow3lem6  19702  lsmval  19718  lsmelval  19719  lsmelvali  19720  lsmelvalm  19721  lsmsubg  19724  lsmub1  19727  lsmub2  19728  lsmless1  19730  lsmless2  19731  lsmless12  19732  lsmass  19739  subglsm  19743  lsmmod  19745  cntzrecd  19748  lsmcntz  19749  lsmcntzr  19750  lsmdisj2  19752  subgdisj1  19761  pj1f  19767  pj1id  19769  pj1lid  19771  pj1rid  19772  pj1ghm  19773  qusecsub  19905  subgabl  19906  ablcntzd  19927  lsmcom  19928  dprdff  20084  dprdfadd  20092  dprdres  20100  dprdss  20101  subgdmdprd  20106  dprdcntz2  20110  dmdprdsplit2lem  20117  ablfacrp  20138  ablfac1eu  20145  pgpfac1lem1  20146  pgpfac1lem2  20147  pgpfac1lem3a  20148  pgpfac1lem3  20149  pgpfac1lem4  20150  pgpfac1lem5  20151  pgpfaclem1  20153  pgpfaclem2  20154  pgpfaclem3  20155  ablfaclem3  20159  ablfac2  20161  prmgrpsimpgd  20186  issubrng2  20643  issubrg2  20677  issubrg3  20685  islss4  21061  dflidl2rng  21321  df2idl2crng  21392  qsnzr  21452  phssip  21777  mpllsslem  22118  subgtgp  24231  subgntr  24233  opnsubg  24234  clssubg  24235  clsnsg  24236  cldsubg  24237  qustgpopn  24246  qustgphaus  24249  tgptsmscls  24276  subgnm  24759  subgngp  24761  lssnlm  24827  cmscsscms  25501  efgh  26672  efabl  26681  efsubm  26682  subgmulgcld  33304  gsumsubg  33307  qusker  33612  eqgvscpbl  33613  grplsmid  33657  quslsm  33658  qusima  33661  nsgmgc  33665  nsgqusf1olem1  33666  nsgqusf1olem2  33667  nsgqusf1olem3  33668  opprqusplusg  33716  opprqus0g  33717  algextdeglem1  34052  algextdeglem2  34053  algextdeglem3  34054  algextdeglem4  34055  algextdeglem5  34056  nelsubgcld  43161  nelsubgsubcld  43162  idomsubgmo  43812