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 5563 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | |
2 | xpeq2 5570 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷)) | |
3 | 1, 2 | sylan9eq 2876 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1533 × cxp 5547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-opab 5121 df-xp 5555 |
This theorem is referenced by: xpeq12i 5577 xpeq12d 5580 xpid11 5796 xp11 6026 infxpenlem 9433 fpwwe2lem5 10050 pwfseqlem4a 10077 pwfseqlem4 10078 pwfseqlem5 10079 pwfseq 10080 pwsval 16753 mamufval 20990 mvmulfval 21145 txtopon 22193 txbasval 22208 txindislem 22235 ismet 22927 isxmet 22928 shsval 29083 sat1el2xp 32621 bj-imdirval 34466 prdsbnd2 35067 ismgmOLD 35122 opidon2OLD 35126 ttac 39626 rfovd 40340 fsovrfovd 40348 sblpnf 40635 |
Copyright terms: Public domain | W3C validator |