Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s2 Structured version   Visualization version   GIF version

Definition df-s2 13444
 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 13437 . 2 class ⟨“𝐴𝐵”⟩
41cs1 13149 . . 3 class ⟨“𝐴”⟩
52cs1 13149 . . 3 class ⟨“𝐵”⟩
6 cconcat 13148 . . 3 class ++
74, 5, 6co 6549 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1475 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
 Colors of variables: wff setvar class This definition is referenced by:  cats2cat  13458  s2eqd  13459  s2cld  13466  s2cli  13475  s2fv0  13482  s2fv1  13483  s2len  13484  s2prop  13502  s2co  13515  s1s2  13518  s2s2  13524  s4s2  13525  s2s5  13529  s5s2  13530  s2eq2s1eq  13531  swrds2  13533  repsw2  13541  ccatw2s1ccatws2  13545  ofs2  13558  gsumws2  17202  efginvrel2  17963  efgredlemc  17981  frgpnabllem1  18099  konigsberg  26514  ofcs2  29948  2pthon3v-av  41150  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424
 Copyright terms: Public domain W3C validator