Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xpeq12d | Structured version Visualization version GIF version |
Description: Equality deduction for Cartesian product. (Contributed by NM, 8-Dec-2013.) |
Ref | Expression |
---|---|
xpeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
xpeq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
xpeq12d | ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | xpeq12d.2 | . 2 ⊢ (𝜑 → 𝐶 = 𝐷) | |
3 | xpeq12 5576 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 587 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 × cxp 5549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-opab 5116 df-xp 5557 |
This theorem is referenced by: sqxpeqd 5583 opeliunxp 5616 mpomptsx 7834 dmmpossx 7836 fmpox 7837 ovmptss 7861 fparlem3 7882 fparlem4 7883 erssxp 8414 marypha2lem2 9052 ackbij1lem8 9841 r1om 9858 fictb 9859 axcc2lem 10050 axcc2 10051 axdc4lem 10069 fsum2dlem 15334 fsumcom2 15338 ackbijnn 15392 fprod2dlem 15542 fprodcom2 15546 homaval 17537 xpcval 17684 xpchom 17687 xpchom2 17693 1stfval 17698 2ndfval 17701 xpcpropd 17716 evlfval 17725 efmnd 18297 isga 18685 gsumcom2 19360 gsumxp 19361 ablfaclem3 19474 psrval 20874 mamufval 21284 mamudm 21287 mvmulfval 21439 mavmuldm 21447 mavmul0g 21450 txbas 22464 ptbasfi 22478 txindis 22531 tmsxps 23434 metustexhalf 23454 aciunf1lem 30719 gsumpart 31034 fedgmullem1 31424 esum2dlem 31772 lpadval 32368 cvmliftlem15 32973 mexval 33177 mpstval 33210 mclsval 33238 mclsax 33244 mclsppslem 33258 on2recsov 33564 naddcllem 33568 noxpordpred 33847 filnetlem4 34307 poimirlem26 35540 poimirlem28 35542 heiborlem3 35708 elrefrels2 36372 refreleq 36375 elcnvrefrels2 36385 dvhfset 38831 dvhset 38832 dibffval 38891 dibfval 38892 hdmap1fval 39547 opeliun2xp 45341 dmmpossx2 45345 functhinclem1 45995 functhinclem3 45997 functhinclem4 45998 |
Copyright terms: Public domain | W3C validator |