![]() |
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 5460 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1520 × cxp 5433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-12 2139 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-opab 5019 df-xp 5441 |
This theorem is referenced by: sqxpeqd 5467 opeliunxp 5497 mpomptsx 7609 dmmpossx 7611 fmpox 7612 ovmptss 7635 fparlem3 7656 fparlem4 7657 erssxp 8153 marypha2lem2 8736 ackbij1lem8 9484 r1om 9501 fictb 9502 axcc2lem 9693 axcc2 9694 axdc4lem 9712 fsum2dlem 14946 fsumcom2 14950 ackbijnn 15004 fprod2dlem 15155 fprodcom2 15159 homaval 17108 xpcval 17244 xpchom 17247 xpchom2 17253 1stfval 17258 2ndfval 17261 xpcpropd 17275 evlfval 17284 isga 18150 symgval 18226 gsumcom2 18803 gsumxp 18804 ablfaclem3 18914 psrval 19818 mamufval 20666 mamudm 20669 mvmulfval 20823 mavmuldm 20831 mavmul0g 20834 txbas 21847 ptbasfi 21861 txindis 21914 tmsxps 22817 metustexhalf 22837 aciunf1lem 30070 fedgmullem1 30584 esum2dlem 30924 lpadval 31520 cvmliftlem15 32109 mexval 32302 mpstval 32335 mclsval 32363 mclsax 32369 mclsppslem 32383 filnetlem4 33283 poimirlem26 34395 poimirlem28 34397 heiborlem3 34569 elrefrels2 35238 refreleq 35241 elcnvrefrels2 35251 dvhfset 37697 dvhset 37698 dibffval 37757 dibfval 37758 hdmap1fval 38413 opeliun2xp 43813 dmmpossx2 43817 |
Copyright terms: Public domain | W3C validator |