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 14887
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 14880 . 2 class ⟨“𝐴𝐵”⟩
41cs1 14633 . . 3 class ⟨“𝐴”⟩
52cs1 14633 . . 3 class ⟨“𝐵”⟩
6 cconcat 14608 . . 3 class ++
74, 5, 6co 7431 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1540 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  14901  s2eqd  14902  s2cld  14910  s2cli  14919  s2fv0  14926  s2fv1  14927  s2len  14928  s2prop  14946  s2co  14959  s1s2  14962  s2s2  14968  s4s2  14969  s2s5  14973  s5s2  14974  s2eq2s1eq  14975  swrds2  14979  repsw2  14989  ccatw2s1ccatws2  14993  s2rn  15002  ofs2  15010  gsumws2  18855  efginvrel2  19745  efgredlemc  19763  frgpnabllem1  19891  2pthon3v  29963  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  cshw1s2  32945  ofcs2  34560
  Copyright terms: Public domain W3C validator