|   | 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 5698 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
| 2 | xpeq2 5705 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷)) | |
| 3 | 1, 2 | sylan9eq 2796 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 × cxp 5682 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-opab 5205 df-xp 5690 | 
| This theorem is referenced by: xpeq12i 5712 xpeq12d 5715 xpid11 5942 xp11 6194 infxpenlem 10054 pwfseqlem4a 10702 pwfseqlem4 10703 pwfseqlem5 10704 pwfseq 10705 pwsval 17532 mamufval 22397 mvmulfval 22549 txtopon 23600 txbasval 23615 txindislem 23642 ismet 24334 isxmet 24335 shsval 31332 sat1el2xp 35385 bj-imdirvallem 37182 prdsbnd2 37803 ismgmOLD 37858 opidon2OLD 37862 ttac 43053 rfovd 44019 fsovrfovd 44027 sblpnf 44334 | 
| Copyright terms: Public domain | W3C validator |