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

Theorem seq3feq 10238
 Description: Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.)
Hypotheses
Ref Expression
seq3feq.1
seq3feq.f
seq3feq.2
seq3feq.pl
Assertion
Ref Expression
seq3feq
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,

Proof of Theorem seq3feq
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2137 . . . 4
2 seq3feq.1 . . . 4
3 seq3feq.f . . . 4
4 seq3feq.pl . . . 4
51, 2, 3, 4seqf 10227 . . 3
65ffnd 5268 . 2
7 fveq2 5414 . . . . . . 7
8 fveq2 5414 . . . . . . 7
97, 8eqeq12d 2152 . . . . . 6
10 seq3feq.2 . . . . . . . 8
1110ralrimiva 2503 . . . . . . 7
1211adantr 274 . . . . . 6
13 simpr 109 . . . . . 6
149, 12, 13rspcdva 2789 . . . . 5
1514, 3eqeltrrd 2215 . . . 4
161, 2, 15, 4seqf 10227 . . 3
1716ffnd 5268 . 2
18 simpr 109 . . 3
19 simpll 518 . . . 4
20 elfzuz 9795 . . . . 5
2120adantl 275 . . . 4
2219, 21, 10syl2anc 408 . . 3