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 18271 | . 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
3 | 2 | simp2bi 1143 | 1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 ⊆ wss 3881 ‘cfv 6324 (class class class)co 7135 Basecbs 16475 ↾s cress 16476 Grpcgrp 18095 SubGrpcsubg 18265 |
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 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 |
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 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fv 6332 df-ov 7138 df-subg 18268 |
This theorem is referenced by: subgbas 18275 subg0 18277 subginv 18278 subgsubcl 18282 subgsub 18283 subgmulgcl 18284 subgmulg 18285 issubg2 18286 issubg4 18290 subsubg 18294 subgint 18295 trivsubgd 18297 nsgconj 18303 nsgacs 18306 ssnmz 18310 eqger 18322 eqgid 18324 eqgen 18325 eqgcpbl 18326 lagsubg2 18333 lagsubg 18334 resghm 18366 ghmnsgima 18374 conjsubg 18382 conjsubgen 18383 conjnmz 18384 conjnmzb 18385 gicsubgen 18410 subgga 18422 gasubg 18424 gastacos 18432 orbstafun 18433 cntrsubgnsg 18463 oddvds2 18685 subgpgp 18714 odcau 18721 pgpssslw 18731 sylow2blem1 18737 sylow2blem2 18738 sylow2blem3 18739 slwhash 18741 fislw 18742 sylow2 18743 sylow3lem1 18744 sylow3lem2 18745 sylow3lem3 18746 sylow3lem4 18747 sylow3lem5 18748 sylow3lem6 18749 lsmval 18765 lsmelval 18766 lsmelvali 18767 lsmelvalm 18768 lsmsubg 18771 lsmub1 18774 lsmub2 18775 lsmless1 18777 lsmless2 18778 lsmless12 18779 lsmass 18787 subglsm 18791 lsmmod 18793 cntzrecd 18796 lsmcntz 18797 lsmcntzr 18798 lsmdisj2 18800 subgdisj1 18809 pj1f 18815 pj1id 18817 pj1lid 18819 pj1rid 18820 pj1ghm 18821 subgabl 18949 ablcntzd 18970 lsmcom 18971 dprdff 19127 dprdfadd 19135 dprdres 19143 dprdss 19144 subgdmdprd 19149 dprdcntz2 19153 dmdprdsplit2lem 19160 ablfacrp 19181 ablfac1eu 19188 pgpfac1lem1 19189 pgpfac1lem2 19190 pgpfac1lem3a 19191 pgpfac1lem3 19192 pgpfac1lem4 19193 pgpfac1lem5 19194 pgpfaclem1 19196 pgpfaclem2 19197 pgpfaclem3 19198 ablfaclem3 19202 ablfac2 19204 prmgrpsimpgd 19229 issubrg2 19548 issubrg3 19556 islss4 19727 phssip 20347 mpllsslem 20673 subgtgp 22710 subgntr 22712 opnsubg 22713 clssubg 22714 clsnsg 22715 cldsubg 22716 qustgpopn 22725 qustgphaus 22728 tgptsmscls 22755 subgnm 23239 subgngp 23241 lssnlm 23307 cmscsscms 23977 efgh 25133 efabl 25142 efsubm 25143 gsumsubg 30731 qusker 30969 eqgvscpbl 30970 nelsubgcld 39424 nelsubgsubcld 39425 idomsubgmo 40142 |
Copyright terms: Public domain | W3C validator |