Theorem grpinvcl 13120

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 13119	. 2 |- ( G e. Grp -> N : B --> B )
4	3	ffvelcdmda 5693	1 |- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   e. wcel 2164   ` cfv 5254   Basecbs 12618   Grpcgrp 13072   invgcminusg 13073

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-riota 5873  df-ov 5921  df-inn 8983  df-2 9041  df-ndx 12621  df-slot 12622  df-base 12624  df-plusg 12708  df-0g 12869  df-mgm 12939  df-sgrp 12985  df-mnd 12998  df-grp 13075  df-minusg 13076

This theorem is referenced by:  grpinvcld  13121  grprinv  13123  grpinvid1  13124  grpinvid2  13125  grplrinv  13129  grpressid  13133  grplcan  13134  grpasscan1  13135  grpasscan2  13136  grpinvinv  13139  grpinvcnv  13140  grpinvnzcl  13144  grpsubinv  13145  grplmulf1o  13146  grpinvssd  13149  grpinvadd  13150  grpsubf  13151  grpsubrcan  13153  grpinvsub  13154  grpinvval2  13155  grpsubeq0  13158  grpsubadd  13160  grpaddsubass  13162  grpnpcan  13164  dfgrp3m  13171  grplactcnv  13174  grpsubpropd2  13177  imasgrp  13181  ghmgrp  13188  mulgcl  13209  mulgaddcomlem  13215  mulginvcom  13217  mulginvinv  13218  mulgneg2  13226  subginv  13251  subginvcl  13253  issubg4m  13263  grpissubg  13264  subgintm  13268  0subg  13269  isnsg3  13277  nmzsubg  13280  eqger  13294  eqglact  13295  eqgcpbl  13298  qusgrp  13302  qusinv  13306  qussub  13307  ghminv  13320  ghmsub  13321  ghmrn  13327  ghmpreima  13336  ghmeql  13337  conjghm  13346  ablinvadd  13380  ablsub2inv  13381  ablsub4  13383  ablsubsub4  13389  invghm  13399  eqgabl  13400  ringnegl  13547  ringnegr  13548  ringmneg1  13549  ringmneg2  13550  ringm2neg  13551  ringsubdi  13552  ringsubdir  13553  dvdsrneg  13599  unitinvcl  13619  unitnegcl  13626  lmodvnegcl  13824  lmodvneg1  13826  lmodvsneg  13827  lmodsubvs  13839  lmodsubdi  13840  lmodsubdir  13841  lssvsubcl  13862  lssvnegcl  13872  lspsnneg  13916