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 5574 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 × cxp 5547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-opab 5121 df-xp 5555 |
This theorem is referenced by: sqxpeqd 5581 opeliunxp 5613 mpomptsx 7753 dmmpossx 7755 fmpox 7756 ovmptss 7779 fparlem3 7800 fparlem4 7801 erssxp 8302 marypha2lem2 8889 ackbij1lem8 9638 r1om 9655 fictb 9656 axcc2lem 9847 axcc2 9848 axdc4lem 9866 fsum2dlem 15115 fsumcom2 15119 ackbijnn 15173 fprod2dlem 15324 fprodcom2 15328 homaval 17281 xpcval 17417 xpchom 17420 xpchom2 17426 1stfval 17431 2ndfval 17434 xpcpropd 17448 evlfval 17457 isga 18361 symgval 18437 gsumcom2 19026 gsumxp 19027 ablfaclem3 19140 psrval 20072 mamufval 20926 mamudm 20929 mvmulfval 21081 mavmuldm 21089 mavmul0g 21092 txbas 22105 ptbasfi 22119 txindis 22172 tmsxps 23075 metustexhalf 23095 aciunf1lem 30336 fedgmullem1 30925 esum2dlem 31251 lpadval 31847 cvmliftlem15 32443 mexval 32647 mpstval 32680 mclsval 32708 mclsax 32714 mclsppslem 32728 filnetlem4 33627 poimirlem26 34800 poimirlem28 34802 heiborlem3 34974 elrefrels2 35639 refreleq 35642 elcnvrefrels2 35652 dvhfset 38098 dvhset 38099 dibffval 38158 dibfval 38159 hdmap1fval 38814 efmnd 43939 opeliun2xp 44279 dmmpossx2 44283 |
Copyright terms: Public domain | W3C validator |