| 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 5710 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) | |
| 4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 × cxp 5683 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-opab 5206 df-xp 5691 |
| This theorem is referenced by: sqxpeqd 5717 opeliunxp 5752 opeliun2xp 5753 mpomptsx 8089 dmmpossx 8091 fmpox 8092 ovmptss 8118 fparlem3 8139 fparlem4 8140 on2recsov 8706 naddcllem 8714 erssxp 8768 marypha2lem2 9476 ackbij1lem8 10266 r1om 10283 fictb 10284 axcc2lem 10476 axcc2 10477 axdc4lem 10495 fsum2dlem 15806 fsumcom2 15810 ackbijnn 15864 fprod2dlem 16016 fprodcom2 16020 homaval 18076 xpcval 18222 xpchom 18225 xpchom2 18231 1stfval 18236 2ndfval 18239 xpcpropd 18253 evlfval 18262 efmnd 18883 isga 19309 gsumcom2 19993 gsumxp 19994 ablfaclem3 20107 psrval 21935 mamufval 22396 mamudm 22399 mvmulfval 22548 mavmuldm 22556 mavmul0g 22559 txbas 23575 ptbasfi 23589 txindis 23642 tmsxps 24549 metustexhalf 24569 noxpordpred 27986 aciunf1lem 32672 gsumpart 33060 gsumwrd2dccatlem 33069 gsumwrd2dccat 33070 erlval 33262 rlocval 33263 fedgmullem1 33680 fldextrspunlsplem 33723 esum2dlem 34093 lpadval 34691 cvmliftlem15 35303 mexval 35507 mpstval 35540 mclsval 35568 mclsax 35574 mclsppslem 35588 filnetlem4 36382 poimirlem26 37653 poimirlem28 37655 heiborlem3 37820 cnvref4 38351 elrefrels2 38519 refreleq 38522 elcnvrefrels2 38535 dvhfset 41082 dvhset 41083 dibffval 41142 dibfval 41143 hdmap1fval 41798 dmmpossx2 48253 swapf2f1oaALT 48984 fucofvalg 49013 fucofvalne 49020 fucof21 49042 functhinclem1 49093 functhinclem3 49095 functhinclem4 49096 |
| Copyright terms: Public domain | W3C validator |