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 13390
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 13383 . 2 class ⟨“𝐴𝐵”⟩
41cs1 13095 . . 3 class ⟨“𝐴”⟩
52cs1 13095 . . 3 class ⟨“𝐵”⟩
6 cconcat 13094 . . 3 class ++
74, 5, 6co 6527 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1474 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  13404  s2eqd  13405  s2cld  13412  s2cli  13421  s2fv0  13428  s2fv1  13429  s2len  13430  s2prop  13448  s2co  13461  s1s2  13464  s2s2  13470  s4s2  13471  s2s5  13475  s5s2  13476  s2eq2s1eq  13477  swrds2  13479  repsw2  13487  ccatw2s1ccatws2  13491  ofs2  13504  gsumws2  17148  efginvrel2  17909  efgredlemc  17927  frgpnabllem1  18045  konigsberg  26280  ofcs2  29754  2pthon3v-av  41145  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419
  Copyright terms: Public domain W3C validator