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 5058 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 691 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 × cxp 5036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-opab 4644 df-xp 5044 |
This theorem is referenced by: sqxpeqd 5065 opeliunxp 5093 mpt2mptsx 7122 dmmpt2ssx 7124 fmpt2x 7125 ovmptss 7145 fparlem3 7166 fparlem4 7167 erssxp 7652 marypha2lem2 8225 ackbij1lem8 8932 r1om 8949 fictb 8950 axcc2lem 9141 axcc2 9142 axdc4lem 9160 fsum2dlem 14343 fsumcom2 14347 fsumcom2OLD 14348 ackbijnn 14399 fprod2dlem 14549 fprodcom2 14553 fprodcom2OLD 14554 homaval 16504 xpcval 16640 xpchom 16643 xpchom2 16649 1stfval 16654 2ndfval 16657 xpcpropd 16671 evlfval 16680 isga 17547 symgval 17622 gsumcom2 18197 gsumxp 18198 ablfaclem3 18309 psrval 19183 mamufval 20010 mamudm 20013 mvmulfval 20167 mavmuldm 20175 mavmul0g 20178 txbas 21180 ptbasfi 21194 txindis 21247 tmsxps 22151 metustexhalf 22171 is2wlkonot 26390 is2spthonot 26391 2wlksot 26394 2spthsot 26395 2wlkonot3v 26402 2spthonot3v 26403 aciunf1lem 28844 esum2dlem 29481 cvmliftlem15 30534 mexval 30653 mpstval 30686 mclsval 30714 mclsax 30720 mclsppslem 30734 filnetlem4 31546 poimirlem26 32605 poimirlem28 32607 heiborlem3 32782 dvhfset 35387 dvhset 35388 dibffval 35447 dibfval 35448 hdmap1fval 36104 opeliun2xp 41904 dmmpt2ssx2 41908 |
Copyright terms: Public domain | W3C validator |