Theorem grpoidcl 23839

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.)

Hypotheses

Ref	Expression
grpoidval.1	|- X = ran G
grpoidval.2	|- U = (GId ` G )

Assertion

Ref	Expression
grpoidcl	|- ( G e. GrpOp -> U e. X )

Proof of Theorem grpoidcl

Dummy variables x u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		grpoidval.1	. . 3 |- X = ran G
2		grpoidval.2	. . 3 |- U = (GId ` G )
3	1, 2	grpoidval 23838	. 2 |- ( G e. GrpOp -> U = ( iota_ u e. X A. x e. X ( u G x ) = x ) )
4	1	grpoideu 23831	. . 3 |- ( G e. GrpOp -> E! u e. X A. x e. X ( u G x ) = x )
5		riotacl 6166	. . 3 |- ( E! u e. X A. x e. X ( u G x ) = x -> ( iota_ u e. X A. x e. X ( u G x ) = x ) e. X )
6	4, 5	syl 16	. 2 |- ( G e. GrpOp -> ( iota_ u e. X A. x e. X ( u G x ) = x ) e. X )
7	3, 6	eqeltrd 2539	1 |- ( G e. GrpOp -> U e. X )

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758   A.wral 2795   E!wreu 2797   ran crn 4939   ` cfv 5516   iota_crio 6150  (class class class)co 6190   GrpOpcgr 23808  GIdcgi 23809

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