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𝑀( + , 𝐹) = seq𝑀( + , 𝐹, V)

Detailed syntax breakdown of Definition df-seq3

Step	Hyp	Ref	Expression
1		c.pl	. . 3 class +
2		cF	. . 3 class 𝐹
3		cM	. . 3 class 𝑀
4	1, 2, 3	cseq 9852	. 2 class seq𝑀( + , 𝐹)
5		cvv 2619	. . 3 class V
6	1, 5, 2, 3	cseq4 9851	. 2 class seq𝑀( + , 𝐹, V)
7	4, 6	wceq 1289	1 wff seq𝑀( + , 𝐹) = seq𝑀( + , 𝐹, V)

This definition is referenced by:  dfseq3-2  9855  seqex  9857  seqeq1  9861  seqeq2  9862  seqeq3  9863  nfseq  9869  seq3feq  9897  seq3shft2  9899  iseqseq3  9902