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 5052 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
2 | xpeq2 5053 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷)) | |
3 | 1, 2 | sylan9eq 2664 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = 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: xpeq12i 5061 xpeq12d 5064 xpid11 5268 xp11 5488 infxpenlem 8719 fpwwe2lem5 9335 pwfseqlem4a 9362 pwfseqlem4 9363 pwfseqlem5 9364 pwfseq 9365 pwsval 15969 mamufval 20010 mvmulfval 20167 txtopon 21204 txbasval 21219 txindislem 21246 ismet 21938 isxmet 21939 shsval 27555 prdsbnd2 32764 ismgmOLD 32819 opidon2OLD 32823 ttac 36621 rfovd 37315 fsovrfovd 37323 sblpnf 37531 |
Copyright terms: Public domain | W3C validator |