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 14201
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 14194 . 2 class ⟨“𝐴𝐵”⟩
41cs1 13940 . . 3 class ⟨“𝐴”⟩
52cs1 13940 . . 3 class ⟨“𝐵”⟩
6 cconcat 13913 . . 3 class ++
74, 5, 6co 7135 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1538 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  14215  s2eqd  14216  s2cld  14224  s2cli  14233  s2fv0  14240  s2fv1  14241  s2len  14242  s2prop  14260  s2co  14273  s1s2  14276  s2s2  14282  s4s2  14283  s2s5  14287  s5s2  14288  s2eq2s1eq  14289  swrds2  14293  repsw2  14303  ccatw2s1ccatws2  14307  ccatw2s1ccatws2OLD  14308  ofs2  14322  gsumws2  17999  efginvrel2  18845  efgredlemc  18863  frgpnabllem1  18986  2pthon3v  27729  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  cshw1s2  30660  ofcs2  31925
  Copyright terms: Public domain W3C validator