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 13639
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 13632 . 2 class ⟨“𝐴𝐵”⟩
41cs1 13326 . . 3 class ⟨“𝐴”⟩
52cs1 13326 . . 3 class ⟨“𝐵”⟩
6 cconcat 13325 . . 3 class ++
74, 5, 6co 6690 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1523 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  13653  s2eqd  13654  s2cld  13662  s2cli  13671  s2fv0  13678  s2fv1  13679  s2len  13680  s2prop  13698  s2co  13711  s1s2  13714  s2s2  13720  s4s2  13721  s2s5  13725  s5s2  13726  s2eq2s1eq  13727  swrds2  13731  repsw2  13739  ccatw2s1ccatws2  13743  ofs2  13756  gsumws2  17426  efginvrel2  18186  efgredlemc  18204  frgpnabllem1  18322  2pthon3v  26908  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  ofcs2  30750
  Copyright terms: Public domain W3C validator