![]() |
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 5692 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
2 | xpeq2 5699 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷)) | |
3 | 1, 2 | sylan9eq 2785 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 × cxp 5676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-opab 5212 df-xp 5684 |
This theorem is referenced by: xpeq12i 5706 xpeq12d 5709 xpid11 5934 xp11 6181 infxpenlem 10038 fpwwe2lem4 10659 pwfseqlem4a 10686 pwfseqlem4 10687 pwfseqlem5 10688 pwfseq 10689 pwsval 17471 mamufval 22336 mvmulfval 22488 txtopon 23539 txbasval 23554 txindislem 23581 ismet 24273 isxmet 24274 shsval 31194 sat1el2xp 35117 bj-imdirvallem 36787 prdsbnd2 37396 ismgmOLD 37451 opidon2OLD 37455 ttac 42596 rfovd 43570 fsovrfovd 43578 sblpnf 43886 |
Copyright terms: Public domain | W3C validator |