Theorem grpinvcl 13624

Description: A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.)

Hypotheses

Ref	Expression
grpinvcl.b	|- B = ( Base ` G )
grpinvcl.n	|- N = ( invg ` G )

Assertion

Ref	Expression
grpinvcl	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )

Proof of Theorem grpinvcl

Step	Hyp	Ref	Expression
1		grpinvcl.b	. . 3 |- B = ( Base ` G )
2		grpinvcl.n	. . 3 |- N = ( invg ` G )
3	1, 2	grpinvf 13623	. 2 |- ( G e. Grp -> N : B --> B )
4	3	ffvelcdmda 5778	1 |- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   e. wcel 2200   ` cfv 5324   Basecbs 13075   Grpcgrp 13576   invgcminusg 13577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4202  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-cnex 8116  ax-resscn 8117  ax-1re 8119  ax-addrcl 8122

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-iun 3970  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331  df-fv 5332  df-riota 5966  df-ov 6016  df-inn 9137  df-2 9195  df-ndx 13078  df-slot 13079  df-base 13081  df-plusg 13166  df-0g 13334  df-mgm 13432  df-sgrp 13478  df-mnd 13493  df-grp 13579  df-minusg 13580

This theorem is referenced by:  grpinvcld  13625  grprinv  13627  grpinvid1  13628  grpinvid2  13629  grplrinv  13633  grpressid  13637  grplcan  13638  grpasscan1  13639  grpasscan2  13640  grpinvinv  13643  grpinvcnv  13644  grpinvnzcl  13648  grpsubinv  13649  grplmulf1o  13650  grpinvssd  13653  grpinvadd  13654  grpsubf  13655  grpsubrcan  13657  grpinvsub  13658  grpinvval2  13659  grpsubeq0  13662  grpsubadd  13664  grpaddsubass  13666  grpnpcan  13668  dfgrp3m  13675  grplactcnv  13678  grpsubpropd2  13681  pwssub  13689  imasgrp  13691  ghmgrp  13698  mulgcl  13719  mulgaddcomlem  13725  mulginvcom  13727  mulginvinv  13728  mulgneg2  13736  subginv  13761  subginvcl  13763  issubg4m  13773  grpissubg  13774  subgintm  13778  0subg  13779  isnsg3  13787  nmzsubg  13790  eqger  13804  eqglact  13805  eqgcpbl  13808  qusgrp  13812  qusinv  13816  qussub  13817  ghminv  13830  ghmsub  13831  ghmrn  13837  ghmpreima  13846  ghmeql  13847  conjghm  13856  ablinvadd  13890  ablsub2inv  13891  ablsub4  13893  ablsubsub4  13899  invghm  13909  eqgabl  13910  ringnegl  14057  ringnegr  14058  ringmneg1  14059  ringmneg2  14060  ringm2neg  14061  ringsubdi  14062  ringsubdir  14063  dvdsrneg  14110  unitinvcl  14130  unitnegcl  14137  lmodvnegcl  14335  lmodvneg1  14337  lmodvsneg  14338  lmodsubvs  14350  lmodsubdi  14351  lmodsubdir  14352  lssvsubcl  14373  lssvnegcl  14383  lspsnneg  14427  psrlinv  14691