![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subgss | Structured version Visualization version GIF version |
Description: A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.) |
Ref | Expression |
---|---|
issubg.b | ⊢ 𝐵 = (Base‘𝐺) |
Ref | Expression |
---|---|
subgss | ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issubg.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
2 | 1 | issubg 17978 | . 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
3 | 2 | simp2bi 1137 | 1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 ⊆ wss 3792 ‘cfv 6135 (class class class)co 6922 Basecbs 16255 ↾s cress 16256 Grpcgrp 17809 SubGrpcsubg 17972 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-mpt 4966 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-iota 6099 df-fun 6137 df-fv 6143 df-ov 6925 df-subg 17975 |
This theorem is referenced by: subgbas 17982 subg0 17984 subginv 17985 subgsubcl 17989 subgsub 17990 subgmulgcl 17991 subgmulg 17992 issubg2 17993 issubg4 17997 subsubg 18001 subgint 18002 nsgconj 18011 nsgacs 18014 ssnmz 18020 eqger 18028 eqgid 18030 eqgen 18031 eqgcpbl 18032 lagsubg2 18039 lagsubg 18040 resghm 18060 ghmnsgima 18068 conjsubg 18076 conjsubgen 18077 conjnmz 18078 conjnmzb 18079 gicsubgen 18104 subgga 18116 gasubg 18118 gastacos 18126 orbstafun 18127 cntrsubgnsg 18156 oddvds2 18367 subgpgp 18396 odcau 18403 pgpssslw 18413 sylow2blem1 18419 sylow2blem2 18420 sylow2blem3 18421 slwhash 18423 fislw 18424 sylow2 18425 sylow3lem1 18426 sylow3lem2 18427 sylow3lem3 18428 sylow3lem4 18429 sylow3lem5 18430 sylow3lem6 18431 lsmval 18447 lsmelval 18448 lsmelvali 18449 lsmelvalm 18450 lsmsubg 18453 lsmub1 18455 lsmub2 18456 lsmless1 18458 lsmless2 18459 lsmless12 18460 lsmass 18467 subglsm 18470 lsmmod 18472 cntzrecd 18475 lsmcntz 18476 lsmcntzr 18477 lsmdisj2 18479 subgdisj1 18488 pj1f 18494 pj1id 18496 pj1lid 18498 pj1rid 18499 pj1ghm 18500 subgabl 18627 ablcntzd 18646 lsmcom 18647 dprdff 18798 dprdfadd 18806 dprdres 18814 dprdss 18815 subgdmdprd 18820 dprdcntz2 18824 dmdprdsplit2lem 18831 ablfacrp 18852 ablfac1eu 18859 pgpfac1lem1 18860 pgpfac1lem2 18861 pgpfac1lem3a 18862 pgpfac1lem3 18863 pgpfac1lem4 18864 pgpfac1lem5 18865 pgpfaclem1 18867 pgpfaclem2 18868 pgpfaclem3 18869 ablfaclem3 18873 ablfac2 18875 issubrg2 19192 issubrg3 19200 islss4 19357 mpllsslem 19832 phssip 20401 subgtgp 22317 subgntr 22318 opnsubg 22319 clssubg 22320 clsnsg 22321 cldsubg 22322 qustgpopn 22331 qustgphaus 22334 tgptsmscls 22361 subgnm 22845 subgngp 22847 lssnlm 22913 cmscsscms 23579 efgh 24725 efabl 24734 efsubm 24735 qusker 30407 eqgvscpbl 30408 nelsubgcld 38134 nelsubgsubcld 38135 idomsubgmo 38739 |
Copyright terms: Public domain | W3C validator |