![]() |
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 19049 | . 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
3 | 2 | simp2bi 1145 | 1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2105 ⊆ wss 3948 ‘cfv 6543 (class class class)co 7412 Basecbs 17151 ↾s cress 17180 Grpcgrp 18861 SubGrpcsubg 19043 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fv 6551 df-ov 7415 df-subg 19046 |
This theorem is referenced by: subgbas 19053 subg0 19055 subginv 19056 subgsubcl 19060 subgsub 19061 subgmulgcl 19062 subgmulg 19063 issubg2 19064 issubg4 19068 subsubg 19072 subgint 19073 trivsubgd 19076 nsgconj 19082 nsgacs 19085 ssnmz 19089 eqger 19101 eqgid 19103 eqgen 19104 eqgcpbl 19105 lagsubg2 19116 lagsubg 19117 eqg0subg 19118 resghm 19153 ghmnsgima 19161 conjsubg 19171 conjsubgen 19172 conjnmz 19173 conjnmzb 19174 gicsubgen 19200 subgga 19212 gasubg 19214 gastacos 19222 orbstafun 19223 cntrsubgnsg 19255 oddvds2 19482 subgpgp 19513 odcau 19520 pgpssslw 19530 sylow2blem1 19536 sylow2blem2 19537 sylow2blem3 19538 slwhash 19540 fislw 19541 sylow2 19542 sylow3lem1 19543 sylow3lem2 19544 sylow3lem3 19545 sylow3lem4 19546 sylow3lem5 19547 sylow3lem6 19548 lsmval 19564 lsmelval 19565 lsmelvali 19566 lsmelvalm 19567 lsmsubg 19570 lsmub1 19573 lsmub2 19574 lsmless1 19576 lsmless2 19577 lsmless12 19578 lsmass 19585 subglsm 19589 lsmmod 19591 cntzrecd 19594 lsmcntz 19595 lsmcntzr 19596 lsmdisj2 19598 subgdisj1 19607 pj1f 19613 pj1id 19615 pj1lid 19617 pj1rid 19618 pj1ghm 19619 qusecsub 19751 subgabl 19752 ablcntzd 19773 lsmcom 19774 dprdff 19930 dprdfadd 19938 dprdres 19946 dprdss 19947 subgdmdprd 19952 dprdcntz2 19956 dmdprdsplit2lem 19963 ablfacrp 19984 ablfac1eu 19991 pgpfac1lem1 19992 pgpfac1lem2 19993 pgpfac1lem3a 19994 pgpfac1lem3 19995 pgpfac1lem4 19996 pgpfac1lem5 19997 pgpfaclem1 19999 pgpfaclem2 20000 pgpfaclem3 20001 ablfaclem3 20005 ablfac2 20007 prmgrpsimpgd 20032 issubrng2 20454 issubrg2 20490 issubrg3 20498 islss4 20805 dflidl2lem 21080 dflidl2rng 21119 phssip 21521 mpllsslem 21870 subgtgp 23929 subgntr 23931 opnsubg 23932 clssubg 23933 clsnsg 23934 cldsubg 23935 qustgpopn 23944 qustgphaus 23947 tgptsmscls 23974 subgnm 24462 subgngp 24464 lssnlm 24538 cmscsscms 25221 efgh 26390 efabl 26399 efsubm 26400 gsumsubg 32634 qusker 32900 eqgvscpbl 32901 grplsmid 32954 quslsm 32956 qusima 32959 nsgmgc 32963 nsgqusf1olem1 32964 nsgqusf1olem2 32965 nsgqusf1olem3 32966 ghmquskerlem1 32968 qsnzr 33014 opprqusplusg 33043 opprqus0g 33044 algextdeglem1 33228 algextdeglem2 33229 algextdeglem3 33230 algextdeglem4 33231 algextdeglem5 33232 nelsubgcld 41538 nelsubgsubcld 41539 idomsubgmo 42403 |
Copyright terms: Public domain | W3C validator |