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 13817
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 13810 . 2 class ⟨“𝐴𝐵”⟩
41cs1 13505 . . 3 class ⟨“𝐴”⟩
52cs1 13505 . . 3 class ⟨“𝐵”⟩
6 cconcat 13504 . . 3 class ++
74, 5, 6co 6874 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1637 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  13831  s2eqd  13832  s2cld  13840  s2cli  13849  s2fv0  13856  s2fv1  13857  s2len  13858  s2prop  13876  s2co  13889  s1s2  13892  s2s2  13898  s4s2  13899  s2s5  13903  s5s2  13904  s2eq2s1eq  13905  swrds2  13909  repsw2  13918  ccatw2s1ccatws2  13922  ofs2  13935  gsumws2  17584  efginvrel2  18341  efgredlemc  18359  frgpnabllem1  18477  2pthon3v  27083  konigsberglem1  27425  konigsberglem2  27426  konigsberglem3  27427  ofcs2  30947
  Copyright terms: Public domain W3C validator