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

Theorem seqeq2 10252
 Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
Assertion
Ref Expression
seqeq2

Proof of Theorem seqeq2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 982 . . . . . . 7
21oveqd 5798 . . . . . 6
32opeq2d 3719 . . . . 5
43mpoeq3dva 5842 . . . 4
5 freceq1 6296 . . . 4 frec frec
64, 5syl 14 . . 3 frec frec
76rneqd 4775 . 2 frec frec
8 df-seqfrec 10249 . 2 frec
9 df-seqfrec 10249 . 2 frec
107, 8, 93eqtr4g 2198 1
 Colors of variables: wff set class Syntax hints:   wi 4   w3a 963   wceq 1332   wcel 1481  cvv 2689  cop 3534   crn 4547  cfv 5130  (class class class)co 5781   cmpo 5783  freccfrec 6294  c1 7644   caddc 7646  cuz 9349   cseq 10248 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3079  df-in 3081  df-ss 3088  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-opab 3997  df-mpt 3998  df-cnv 4554  df-dm 4556  df-rn 4557  df-res 4558  df-iota 5095  df-fv 5138  df-ov 5784  df-oprab 5785  df-mpo 5786  df-recs 6209  df-frec 6295  df-seqfrec 10249 This theorem is referenced by:  seqeq2d  10255  resqrex  10829
 Copyright terms: Public domain W3C validator