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 14786
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 14779 . 2 class ⟨“𝐴𝐵”⟩
41cs1 14532 . . 3 class ⟨“𝐴”⟩
52cs1 14532 . . 3 class ⟨“𝐵”⟩
6 cconcat 14507 . . 3 class ++
74, 5, 6co 7396 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1542 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  14800  s2eqd  14801  s2cld  14809  s2cli  14818  s2fv0  14825  s2fv1  14826  s2len  14827  s2prop  14845  s2co  14858  s1s2  14861  s2s2  14867  s4s2  14868  s2s5  14872  s5s2  14873  s2eq2s1eq  14874  swrds2  14878  repsw2  14888  ccatw2s1ccatws2  14892  ofs2  14905  gsumws2  18710  efginvrel2  19579  efgredlemc  19597  frgpnabllem1  19724  2pthon3v  29164  konigsberglem1  29472  konigsberglem2  29473  konigsberglem3  29474  cshw1s2  32095  ofcs2  33487
  Copyright terms: Public domain W3C validator