Metamath Proof Explorer


Theorem prodeq2w

Description: Equality theorem for product, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion prodeq2w kB=CkAB=kAC

Proof

Step Hyp Ref Expression
1 eqid =
2 ifeq1 B=CifkAB1=ifkAC1
3 2 alimi kB=CkifkAB1=ifkAC1
4 alral kifkAB1=ifkAC1kifkAB1=ifkAC1
5 3 4 syl kB=CkifkAB1=ifkAC1
6 mpteq12 =kifkAB1=ifkAC1kifkAB1=kifkAC1
7 1 5 6 sylancr kB=CkifkAB1=kifkAC1
8 7 seqeq3d kB=Cseqn×kifkAB1=seqn×kifkAC1
9 8 breq1d kB=Cseqn×kifkAB1yseqn×kifkAC1y
10 9 anbi2d kB=Cy0seqn×kifkAB1yy0seqn×kifkAC1y
11 10 exbidv kB=Cyy0seqn×kifkAB1yyy0seqn×kifkAC1y
12 11 rexbidv kB=Cnmyy0seqn×kifkAB1ynmyy0seqn×kifkAC1y
13 7 seqeq3d kB=Cseqm×kifkAB1=seqm×kifkAC1
14 13 breq1d kB=Cseqm×kifkAB1xseqm×kifkAC1x
15 12 14 3anbi23d kB=CAmnmyy0seqn×kifkAB1yseqm×kifkAB1xAmnmyy0seqn×kifkAC1yseqm×kifkAC1x
16 15 rexbidv kB=CmAmnmyy0seqn×kifkAB1yseqm×kifkAB1xmAmnmyy0seqn×kifkAC1yseqm×kifkAC1x
17 csbeq2 kB=Cfn/kB=fn/kC
18 17 mpteq2dv kB=Cnfn/kB=nfn/kC
19 18 seqeq3d kB=Cseq1×nfn/kB=seq1×nfn/kC
20 19 fveq1d kB=Cseq1×nfn/kBm=seq1×nfn/kCm
21 20 eqeq2d kB=Cx=seq1×nfn/kBmx=seq1×nfn/kCm
22 21 anbi2d kB=Cf:1m1-1 ontoAx=seq1×nfn/kBmf:1m1-1 ontoAx=seq1×nfn/kCm
23 22 exbidv kB=Cff:1m1-1 ontoAx=seq1×nfn/kBmff:1m1-1 ontoAx=seq1×nfn/kCm
24 23 rexbidv kB=Cmff:1m1-1 ontoAx=seq1×nfn/kBmmff:1m1-1 ontoAx=seq1×nfn/kCm
25 16 24 orbi12d kB=CmAmnmyy0seqn×kifkAB1yseqm×kifkAB1xmff:1m1-1 ontoAx=seq1×nfn/kBmmAmnmyy0seqn×kifkAC1yseqm×kifkAC1xmff:1m1-1 ontoAx=seq1×nfn/kCm
26 25 iotabidv kB=Cιx|mAmnmyy0seqn×kifkAB1yseqm×kifkAB1xmff:1m1-1 ontoAx=seq1×nfn/kBm=ιx|mAmnmyy0seqn×kifkAC1yseqm×kifkAC1xmff:1m1-1 ontoAx=seq1×nfn/kCm
27 df-prod kAB=ιx|mAmnmyy0seqn×kifkAB1yseqm×kifkAB1xmff:1m1-1 ontoAx=seq1×nfn/kBm
28 df-prod kAC=ιx|mAmnmyy0seqn×kifkAC1yseqm×kifkAC1xmff:1m1-1 ontoAx=seq1×nfn/kCm
29 26 27 28 3eqtr4g kB=CkAB=kAC