![]() |
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 5274 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 565 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 × cxp 5247 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-opab 4847 df-xp 5255 |
This theorem is referenced by: sqxpeqd 5281 opeliunxp 5310 mpt2mptsx 7383 dmmpt2ssx 7385 fmpt2x 7386 ovmptss 7409 fparlem3 7430 fparlem4 7431 erssxp 7919 marypha2lem2 8498 ackbij1lem8 9251 r1om 9268 fictb 9269 axcc2lem 9460 axcc2 9461 axdc4lem 9479 fsum2dlem 14709 fsumcom2 14713 ackbijnn 14767 fprod2dlem 14917 fprodcom2 14921 homaval 16888 xpcval 17025 xpchom 17028 xpchom2 17034 1stfval 17039 2ndfval 17042 xpcpropd 17056 evlfval 17065 isga 17931 symgval 18006 gsumcom2 18581 gsumxp 18582 ablfaclem3 18694 psrval 19577 mamufval 20408 mamudm 20411 mvmulfval 20566 mavmuldm 20574 mavmul0g 20577 txbas 21591 ptbasfi 21605 txindis 21658 tmsxps 22561 metustexhalf 22581 aciunf1lem 29802 esum2dlem 30494 cvmliftlem15 31618 mexval 31737 mpstval 31770 mclsval 31798 mclsax 31804 mclsppslem 31818 filnetlem4 32713 poimirlem26 33768 poimirlem28 33770 heiborlem3 33944 elrefrels2 34609 refreleq 34612 elcnvrefrels2 34622 dvhfset 36890 dvhset 36891 dibffval 36950 dibfval 36951 hdmap1fval 37606 opeliun2xp 42639 dmmpt2ssx2 42643 |
Copyright terms: Public domain | W3C validator |