![]() |
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 5699 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 582 | 1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 × cxp 5672 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-opab 5208 df-xp 5680 |
This theorem is referenced by: sqxpeqd 5706 opeliunxp 5741 mpomptsx 8070 dmmpossx 8072 fmpox 8073 ovmptss 8099 fparlem3 8120 fparlem4 8121 on2recsov 8690 naddcllem 8698 erssxp 8749 marypha2lem2 9472 ackbij1lem8 10261 r1om 10278 fictb 10279 axcc2lem 10470 axcc2 10471 axdc4lem 10489 fsum2dlem 15769 fsumcom2 15773 ackbijnn 15827 fprod2dlem 15977 fprodcom2 15981 homaval 18048 xpcval 18196 xpchom 18199 xpchom2 18205 1stfval 18210 2ndfval 18213 xpcpropd 18228 evlfval 18237 efmnd 18855 isga 19281 gsumcom2 19969 gsumxp 19970 ablfaclem3 20083 psrval 21908 mamufval 22380 mamudm 22383 mvmulfval 22532 mavmuldm 22540 mavmul0g 22543 txbas 23559 ptbasfi 23573 txindis 23626 tmsxps 24533 metustexhalf 24553 noxpordpred 27964 aciunf1lem 32579 gsumpart 32927 erlval 33118 rlocval 33119 fedgmullem1 33530 esum2dlem 33938 lpadval 34535 cvmliftlem15 35139 mexval 35343 mpstval 35376 mclsval 35404 mclsax 35410 mclsppslem 35424 filnetlem4 36106 poimirlem26 37360 poimirlem28 37362 heiborlem3 37527 cnvref4 38061 elrefrels2 38229 refreleq 38232 elcnvrefrels2 38245 dvhfset 40792 dvhset 40793 dibffval 40852 dibfval 40853 hdmap1fval 41508 opeliun2xp 47747 dmmpossx2 47751 functhinclem1 48398 functhinclem3 48400 functhinclem4 48401 |
Copyright terms: Public domain | W3C validator |