Metamath Proof Explorer


Theorem sumeq2w

Description: Equality theorem for sum, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion sumeq2w kB=CkAB=kAC

Proof

Step Hyp Ref Expression
1 csbeq2 kB=Cn/kB=n/kC
2 1 ifeq1d kB=CifnAn/kB0=ifnAn/kC0
3 2 mpteq2dv kB=CnifnAn/kB0=nifnAn/kC0
4 3 seqeq3d kB=Cseqm+nifnAn/kB0=seqm+nifnAn/kC0
5 4 breq1d kB=Cseqm+nifnAn/kB0xseqm+nifnAn/kC0x
6 5 anbi2d kB=CAmseqm+nifnAn/kB0xAmseqm+nifnAn/kC0x
7 6 rexbidv kB=CmAmseqm+nifnAn/kB0xmAmseqm+nifnAn/kC0x
8 csbeq2 kB=Cfn/kB=fn/kC
9 8 mpteq2dv kB=Cnfn/kB=nfn/kC
10 9 seqeq3d kB=Cseq1+nfn/kB=seq1+nfn/kC
11 10 fveq1d kB=Cseq1+nfn/kBm=seq1+nfn/kCm
12 11 eqeq2d kB=Cx=seq1+nfn/kBmx=seq1+nfn/kCm
13 12 anbi2d kB=Cf:1m1-1 ontoAx=seq1+nfn/kBmf:1m1-1 ontoAx=seq1+nfn/kCm
14 13 exbidv kB=Cff:1m1-1 ontoAx=seq1+nfn/kBmff:1m1-1 ontoAx=seq1+nfn/kCm
15 14 rexbidv kB=Cmff:1m1-1 ontoAx=seq1+nfn/kBmmff:1m1-1 ontoAx=seq1+nfn/kCm
16 7 15 orbi12d kB=CmAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBmmAmseqm+nifnAn/kC0xmff:1m1-1 ontoAx=seq1+nfn/kCm
17 16 iotabidv kB=Cιx|mAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBm=ιx|mAmseqm+nifnAn/kC0xmff:1m1-1 ontoAx=seq1+nfn/kCm
18 df-sum kAB=ιx|mAmseqm+nifnAn/kB0xmff:1m1-1 ontoAx=seq1+nfn/kBm
19 df-sum kAC=ιx|mAmseqm+nifnAn/kC0xmff:1m1-1 ontoAx=seq1+nfn/kCm
20 17 18 19 3eqtr4g kB=CkAB=kAC