Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cmpidelt Structured version   Visualization version   Unicode version

Theorem cmpidelt 26050
 Description: A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
cmpidelt.1
cmpidelt.2 GId
Assertion
Ref Expression
cmpidelt

Proof of Theorem cmpidelt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cmpidelt.1 . . . . 5
2 cmpidelt.2 . . . . 5 GId
31, 2idrval 26048 . . . 4
43eqcomd 2456 . . 3
51, 2iorlid 26049 . . . 4
61exidu1 26047 . . . 4
7 oveq1 6295 . . . . . . . 8
87eqeq1d 2452 . . . . . . 7
9 oveq2 6296 . . . . . . . 8
109eqeq1d 2452 . . . . . . 7
118, 10anbi12d 716 . . . . . 6
1211ralbidv 2826 . . . . 5
1312riota2 6272 . . . 4
145, 6, 13syl2anc 666 . . 3
154, 14mpbird 236 . 2
16 oveq2 6296 . . . . 5
17 id 22 . . . . 5
1816, 17eqeq12d 2465 . . . 4
19 oveq1 6295 . . . . 5
2019, 17eqeq12d 2465 . . . 4
2118, 20anbi12d 716 . . 3
2221rspccva 3148 . 2
2315, 22sylan 474 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1443   wcel 1886  wral 2736  wreu 2738   cin 3402   crn 4834  cfv 5581  crio 6249  (class class class)co 6288  GIdcgi 25908   cexid 26035  cmagm 26039 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638  ax-un 6580 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-fo 5587  df-fv 5589  df-riota 6250  df-ov 6291  df-gid 25913  df-exid 26036  df-mgmOLD 26040 This theorem is referenced by:  rngoidmlem  26144  exidreslem  32168
 Copyright terms: Public domain W3C validator