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

Theorem ismgmOLD 26033
 Description: Obsolete version of ismgm 16476 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypothesis
Ref Expression
ismgmOLD.1
Assertion
Ref Expression
ismgmOLD

Proof of Theorem ismgmOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 feq1 5724 . . . . 5
21exbidv 1758 . . . 4
3 df-mgmOLD 26032 . . . 4
42, 3elab2g 3220 . . 3
5 f00 5778 . . . . . . . 8
6 dmeq 5050 . . . . . . . . . 10
7 dmeq 5050 . . . . . . . . . . 11
8 dm0 5063 . . . . . . . . . . . . 13
98dmeqi 5051 . . . . . . . . . . . 12
109, 8eqtri 2451 . . . . . . . . . . 11
117, 10syl6req 2480 . . . . . . . . . 10
126, 11syl 17 . . . . . . . . 9
1312adantr 466 . . . . . . . 8
145, 13sylbi 198 . . . . . . 7
15 xpeq12 4868 . . . . . . . . . 10
1615anidms 649 . . . . . . . . 9
17 feq23 5727 . . . . . . . . 9
1816, 17mpancom 673 . . . . . . . 8
19 eqeq1 2426 . . . . . . . 8
2018, 19imbi12d 321 . . . . . . 7
2114, 20mpbiri 236 . . . . . 6
22 fdm 5746 . . . . . . . 8
23 dmeq 5050 . . . . . . . 8
24 df-ne 2620 . . . . . . . . . . . 12
25 dmxp 5068 . . . . . . . . . . . 12
2624, 25sylbir 216 . . . . . . . . . . 11
2726eqeq1d 2424 . . . . . . . . . 10
2827biimpcd 227 . . . . . . . . 9
2928eqcoms 2434 . . . . . . . 8
3022, 23, 293syl 18 . . . . . . 7
3130com12 32 . . . . . 6
3221, 31pm2.61i 167 . . . . 5
3332pm4.71ri 637 . . . 4
3433exbii 1712 . . 3
354, 34syl6bb 264 . 2
36 dmexg 6734 . . 3
37 dmexg 6734 . . 3
38 xpeq12 4868 . . . . . . 7
3938anidms 649 . . . . . 6
40 feq23 5727 . . . . . 6
4139, 40mpancom 673 . . . . 5
42 ismgmOLD.1 . . . . . . . 8
4342eqcomi 2435 . . . . . . 7
4443, 43xpeq12i 4871 . . . . . 6
4544, 43feq23i 5736 . . . . 5
4641, 45syl6bb 264 . . . 4
4746ceqsexgv 3204 . . 3
4836, 37, 473syl 18 . 2
4935, 48bitrd 256 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   wceq 1437  wex 1659   wcel 1868   wne 2618  cvv 3081  c0 3761   cxp 4847   cdm 4849  wf 5593  cmagm 26031 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-fun 5599  df-fn 5600  df-f 5601  df-mgmOLD 26032 This theorem is referenced by:  clmgmOLD  26034  opidonOLD  26035  issmgrpOLD  26047
 Copyright terms: Public domain W3C validator