Theorem grpinvcl 13913

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   ` cfv 5380   Basecbs 13411   Grpcgrp 13865   invgcminusg 13866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4248  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-cnex 8277  ax-resscn 8278  ax-1re 8280  ax-addrcl 8283

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-riota 6041  df-ov 6091  df-inn 9315  df-2 9373  df-ndx 13414  df-slot 13415  df-base 13417  df-plusg 13504  df-0g 13672  df-mgm 13736  df-sgrp 13777  df-mnd 13790  df-grp 13868  df-minusg 13869

This theorem is used by:  grpinvcld  13914  grprinv  13916  grpinvid1  13917  grpinvid2  13918  grplrinv  13922  grpressid  13926  grplcan  13927  grpasscan1  13928  grpasscan2  13929  grpinvinv  13932  grpinvcnv  13933  grpinvnzcl  13937  grpsubinv  13938  grplmulf1o  13939  grpinvssd  13942  grpinvadd  13943  grpsubf  13944  grpsubrcan  13946  grpinvsub  13947  grpinvval2  13948  grpsubeq0  13951  grpsubadd  13953  grpaddsubass  13955  grpnpcan  13957  dfgrp3m  13964  grplactcnv  13967  grpsubpropd2  13970  imasgrp  13974  ghmgrp  13981  mulgcl  14002  mulgaddcomlem  14008  mulginvcom  14010  mulginvinv  14011  mulgneg2  14019  subginv  14044  subginvcl  14046  issubg4m  14056  grpissubg  14057  subgintm  14061  0subg  14062  isnsg3  14070  nmzsubg  14073  eqger  14087  eqglact  14088  eqgcpbl  14091  qusgrp  14095  qusinv  14099  qussub  14100  ghminv  14113  ghmsub  14114  ghmrn  14120  ghmpreima  14129  ghmeql  14130  conjghm  14139  cntzsubg  14172  ablinvadd  14205  ablsub2inv  14206  ablsub4  14208  ablsubsub4  14214  invghm  14224  eqgabl  14225  pwssub  14324  ringnegl  14464  ringnegr  14465  ringmneg1  14466  ringmneg2  14467  ringm2neg  14468  ringsubdi  14469  ringsubdir  14470  dvdsrneg  14520  unitinvcl  14540  unitnegcl  14547  lmodvnegcl  14775  lmodvneg1  14777  lmodvsneg  14778  lmodsubvs  14790  lmodsubdi  14791  lmodsubdir  14792  lssvsubcl  14813  lssvnegcl  14823  lspsnneg  14867  psrlinv  15199