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 13764
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 13757 . 2 class ⟨“𝐴𝐵”⟩
41cs1 13451 . . 3 class ⟨“𝐴”⟩
52cs1 13451 . . 3 class ⟨“𝐵”⟩
6 cconcat 13450 . . 3 class ++
74, 5, 6co 6801 . 2 class (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
83, 7wceq 1620 1 wff ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  cats2cat  13778  s2eqd  13779  s2cld  13787  s2cli  13796  s2fv0  13803  s2fv1  13804  s2len  13805  s2prop  13823  s2co  13836  s1s2  13839  s2s2  13845  s4s2  13846  s2s5  13850  s5s2  13851  s2eq2s1eq  13852  swrds2  13856  repsw2  13865  ccatw2s1ccatws2  13869  ofs2  13882  gsumws2  17551  efginvrel2  18311  efgredlemc  18329  frgpnabllem1  18447  2pthon3v  27034  konigsberglem1  27375  konigsberglem2  27376  konigsberglem3  27377  ofcs2  30902
  Copyright terms: Public domain W3C validator