![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > grpoidcl | Structured version Unicode version |
Description: The identity element of a group belongs to the group. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
Ref | Expression |
---|---|
grpoidval.1 |
![]() ![]() ![]() ![]() ![]() |
grpoidval.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
grpoidcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpoidval.1 |
. . 3
![]() ![]() ![]() ![]() ![]() | |
2 | grpoidval.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | grpoidval 23838 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | grpoideu 23831 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | riotacl 6166 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | syl 16 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | eqeltrd 2539 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4511 ax-nul 4519 ax-pr 4629 ax-un 6472 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3070 df-sbc 3285 df-csb 3387 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-nul 3736 df-if 3890 df-sn 3976 df-pr 3978 df-op 3982 df-uni 4190 df-iun 4271 df-br 4391 df-opab 4449 df-mpt 4450 df-id 4734 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-iota 5479 df-fun 5518 df-fn 5519 df-f 5520 df-fo 5522 df-fv 5524 df-riota 6151 df-ov 6193 df-grpo 23813 df-gid 23814 |
This theorem is referenced by: grpoid 23845 grpoinvid 23854 grpo2grp 23856 gxcl 23887 gxid 23895 gxdi 23918 subgoid 23929 gidsn 23970 ghomid 23987 ghgrp 23990 rngo0cl 24020 rngolz 24023 rngorz 24024 vczcl 24079 nvzcl 24149 ghomgrpilem2 27439 ghomf1olem 27447 grpokerinj 28888 keridl 28970 |
Copyright terms: Public domain | W3C validator |