MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s2 Structured version   Visualization version   GIF version

Definition df-s2 14200
Description: Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s2 ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)

Detailed syntax breakdown of Definition df-s2
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cs2 14193 . 2 class ⟨“𝐴𝐵”⟩
41cs1 13939 . . 3 class ⟨“𝐴”⟩
52cs1 13939 . . 3 class ⟨“𝐵”⟩
6 cconcat 13912 . . 3 class ++
74, 5, 6co 7145 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1528 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  14214  s2eqd  14215  s2cld  14223  s2cli  14232  s2fv0  14239  s2fv1  14240  s2len  14241  s2prop  14259  s2co  14272  s1s2  14275  s2s2  14281  s4s2  14282  s2s5  14286  s5s2  14287  s2eq2s1eq  14288  swrds2  14292  repsw2  14302  ccatw2s1ccatws2  14306  ccatw2s1ccatws2OLD  14307  ofs2  14321  gsumws2  17997  efginvrel2  18784  efgredlemc  18802  frgpnabllem1  18924  2pthon3v  27650  konigsberglem1  27959  konigsberglem2  27960  konigsberglem3  27961  cshw1s2  30562  ofcs2  31715
  Copyright terms: Public domain W3C validator