MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s4 Unicode version

Definition df-s4 12815
Description: Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s4

Detailed syntax breakdown of Definition df-s4
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cC . . 3
4 cD . . 3
51, 2, 3, 4cs4 12808 . 2
61, 2, 3cs3 12807 . . 3
74cs1 12537 . . 3
8 cconcat 12536 . . 3
96, 7, 8co 6296 . 2
105, 9wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  12829  s4cld  12836  s4cli  12845  s4len  12857  s4prop  12863  s1s3  12872  s1s4  12873  s2s2  12877  s4s4  12880  usgraexmplvtx  24402  konigsberg  24987
  Copyright terms: Public domain W3C validator