ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-seq3 Unicode version

Definition df-seq3 9854
Description: Define a three-argument version of  seq. By theorems such as iseqsst 9886, it should be capable of doing pretty much everything that the four-argument version can, and may eventually replace the four-argument version entirely. (Contributed by Jim Kingdon, 3-Oct-2022.)
Assertion
Ref Expression
df-seq3  |-  seq M
(  .+  ,  F
)  =  seq M
(  .+  ,  F ,  _V )

Detailed syntax breakdown of Definition df-seq3
StepHypRef Expression
1 c.pl . . 3  class  .+
2 cF . . 3  class  F
3 cM . . 3  class  M
41, 2, 3cseq 9852 . 2  class  seq M
(  .+  ,  F
)
5 cvv 2619 . . 3  class  _V
61, 5, 2, 3cseq4 9851 . 2  class  seq M
(  .+  ,  F ,  _V )
74, 6wceq 1289 1  wff  seq M
(  .+  ,  F
)  =  seq M
(  .+  ,  F ,  _V )
Colors of variables: wff set class
This definition is referenced by:  dfseq3-2  9855  seqex  9857  seqeq1  9861  seqeq2  9862  seqeq3  9863  nfseq  9869  seq3feq  9897  seq3shft2  9899  iseqseq3  9902
  Copyright terms: Public domain W3C validator