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

Theorem iseqfeq 9617
 Description: Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.)
Hypotheses
Ref Expression
iseqfeq.1
iseqfeq.f
iseqfeq.2
iseqfeq.pl
Assertion
Ref Expression
iseqfeq
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,

Proof of Theorem iseqfeq
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2083 . . . 4
2 iseqfeq.1 . . . 4
3 iseqfeq.f . . . 4
4 iseqfeq.pl . . . 4
51, 2, 3, 4iseqfcl 9605 . . 3
6 ffn 5097 . . 3
75, 6syl 14 . 2
8 iseqfeq.2 . . . . . . 7
98ralrimiva 2439 . . . . . 6
10 fveq2 5230 . . . . . . . 8
11 fveq2 5230 . . . . . . . 8
1210, 11eqeq12d 2097 . . . . . . 7
1312rspcv 2706 . . . . . 6
149, 13mpan9 275 . . . . 5
1514, 3eqeltrrd 2160 . . . 4
161, 2, 15, 4iseqfcl 9605 . . 3
17 ffn 5097 . . 3
1816, 17syl 14 . 2
19 simpr 108 . . 3
20 elfzuz 9187 . . . . 5
2120, 8sylan2 280 . . . 4