Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prodeq2w Structured version   Unicode version

Theorem prodeq2w 13909
 Description: Equality theorem for product, when the class expressions and are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017.)
Assertion
Ref Expression
prodeq2w
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem prodeq2w
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2428 . . . . . . . . . . . 12
2 ifeq1 3858 . . . . . . . . . . . . . 14
32alimi 1678 . . . . . . . . . . . . 13
4 alral 2730 . . . . . . . . . . . . 13
53, 4syl 17 . . . . . . . . . . . 12
6 mpteq12 4446 . . . . . . . . . . . 12
71, 5, 6sylancr 667 . . . . . . . . . . 11
87seqeq3d 12171 . . . . . . . . . 10
98breq1d 4376 . . . . . . . . 9
109anbi2d 708 . . . . . . . 8
1110exbidv 1762 . . . . . . 7
1211rexbidv 2878 . . . . . 6
137seqeq3d 12171 . . . . . . 7
1413breq1d 4376 . . . . . 6
1512, 143anbi23d 1338 . . . . 5
1615rexbidv 2878 . . . 4
17 csbeq2 3342 . . . . . . . . . . 11
1817mpteq2dv 4454 . . . . . . . . . 10
1918seqeq3d 12171 . . . . . . . . 9
2019fveq1d 5827 . . . . . . . 8
2120eqeq2d 2438 . . . . . . 7
2221anbi2d 708 . . . . . 6
2322exbidv 1762 . . . . 5
2423rexbidv 2878 . . . 4
2516, 24orbi12d 714 . . 3
2625iotabidv 5529 . 2
27 df-prod 13903 . 2
28 df-prod 13903 . 2
2926, 27, 283eqtr4g 2487 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 369   wa 370   w3a 982  wal 1435   wceq 1437  wex 1657   wcel 1872   wne 2599  wral 2714  wrex 2715  csb 3338   wss 3379  cif 3854   class class class wbr 4366   cmpt 4425  cio 5506  wf1o 5543  cfv 5544  (class class class)co 6249  cc0 9490  c1 9491   cmul 9495  cn 10560  cz 10888  cuz 11110  cfz 11735   cseq 12163   cli 13491  cprod 13902 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-xp 4802  df-cnv 4804  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-iota 5508  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-seq 12164  df-prod 13903 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator