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

Theorem iseqeq2 9922
 Description: Equality theorem for the sequence builder operation. New proofs should use seqeq2 9925 instead (together with iseqsst 9949 or iseqseq3 9965 if need be). (Contributed by Jim Kingdon, 30-May-2020.) (New usage is discouraged.)
Assertion
Ref Expression
iseqeq2

Proof of Theorem iseqeq2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 944 . . . . . . 7
21oveqd 5685 . . . . . 6
32opeq2d 3637 . . . . 5
43mpt2eq3dva 5729 . . . 4
5 freceq1 6173 . . . 4 frec frec
64, 5syl 14 . . 3 frec frec
76rneqd 4679 . 2 frec frec
8 df-iseq 9916 . 2 frec
9 df-iseq 9916 . 2 frec
107, 8, 93eqtr4g 2146 1
 Colors of variables: wff set class Syntax hints:   wi 4   w3a 925   wceq 1290   wcel 1439  cop 3455   crn 4455  cfv 5030  (class class class)co 5668   cmpt2 5670  freccfrec 6171  c1 7414   caddc 7416  cuz 9082   cseq4 9914 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071 This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2624  df-un 3006  df-in 3008  df-ss 3015  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-br 3854  df-opab 3908  df-mpt 3909  df-cnv 4462  df-dm 4464  df-rn 4465  df-res 4466  df-iota 4995  df-fv 5038  df-ov 5671  df-oprab 5672  df-mpt2 5673  df-recs 6086  df-frec 6172  df-iseq 9916 This theorem is referenced by:  seqeq2  9925
 Copyright terms: Public domain W3C validator