ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-seq3 GIF 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𝑀( + , 𝐹) = seq𝑀( + , 𝐹, V)

Detailed syntax breakdown of Definition df-seq3
StepHypRef Expression
1 c.pl . . 3 class +
2 cF . . 3 class 𝐹
3 cM . . 3 class 𝑀
41, 2, 3cseq 9852 . 2 class seq𝑀( + , 𝐹)
5 cvv 2619 . . 3 class V
61, 5, 2, 3cseq4 9851 . 2 class seq𝑀( + , 𝐹, V)
74, 6wceq 1289 1 wff seq𝑀( + , 𝐹) = seq𝑀( + , 𝐹, 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