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 14198
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 14191 . 2 class ⟨“𝐴𝐵”⟩
41cs1 13937 . . 3 class ⟨“𝐴”⟩
52cs1 13937 . . 3 class ⟨“𝐵”⟩
6 cconcat 13910 . . 3 class ++
74, 5, 6co 7145 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1528 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  14212  s2eqd  14213  s2cld  14221  s2cli  14230  s2fv0  14237  s2fv1  14238  s2len  14239  s2prop  14257  s2co  14270  s1s2  14273  s2s2  14279  s4s2  14280  s2s5  14284  s5s2  14285  s2eq2s1eq  14286  swrds2  14290  repsw2  14300  ccatw2s1ccatws2  14304  ccatw2s1ccatws2OLD  14305  ofs2  14319  gsumws2  17995  efginvrel2  18782  efgredlemc  18800  frgpnabllem1  18922  2pthon3v  27649  konigsberglem1  27958  konigsberglem2  27959  konigsberglem3  27960  cshw1s2  30561  ofcs2  31714
  Copyright terms: Public domain W3C validator