![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpeq12 | Structured version Visualization version GIF version |
Description: Equality theorem for Cartesian product. (Contributed by FL, 31-Aug-2009.) |
Ref | Expression |
---|---|
xpeq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpeq1 5327 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
2 | xpeq2 5334 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷)) | |
3 | 1, 2 | sylan9eq 2854 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 × cxp 5311 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2778 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2787 df-cleq 2793 df-clel 2796 df-opab 4907 df-xp 5319 |
This theorem is referenced by: xpeq12i 5341 xpeq12d 5344 xpid11 5551 xp11 5787 infxpenlem 9123 fpwwe2lem5 9745 pwfseqlem4a 9772 pwfseqlem4 9773 pwfseqlem5 9774 pwfseq 9775 pwsval 16460 mamufval 20515 mvmulfval 20673 txtopon 21722 txbasval 21737 txindislem 21764 ismet 22455 isxmet 22456 shsval 28695 prdsbnd2 34080 ismgmOLD 34135 opidon2OLD 34139 ttac 38383 rfovd 39072 fsovrfovd 39080 sblpnf 39286 |
Copyright terms: Public domain | W3C validator |