![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inxp | Structured version Visualization version GIF version |
Description: Intersection of two Cartesian products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Avoid ax-10 2138, ax-12 2174. (Revised by SN, 5-May-2025.) |
Ref | Expression |
---|---|
inxp | ⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relinxp 5826 | . 2 ⊢ Rel ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) | |
2 | relxp 5706 | . 2 ⊢ Rel ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) | |
3 | an4 656 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))) | |
4 | opelxp 5724 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
5 | opelxp 5724 | . . . . 5 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐶 × 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) | |
6 | 4, 5 | anbi12i 628 | . . . 4 ⊢ ((〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 × 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))) |
7 | elin 3978 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
8 | elin 3978 | . . . . 5 ⊢ (𝑦 ∈ (𝐵 ∩ 𝐷) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)) | |
9 | 7, 8 | anbi12i 628 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))) |
10 | 3, 6, 9 | 3bitr4i 303 | . . 3 ⊢ ((〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 × 𝐷)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷))) |
11 | elin 3978 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) ↔ (〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 × 𝐷))) | |
12 | opelxp 5724 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷))) | |
13 | 10, 11, 12 | 3bitr4i 303 | . 2 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) ↔ 〈𝑥, 𝑦〉 ∈ ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷))) |
14 | 1, 2, 13 | eqrelriiv 5802 | 1 ⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1536 ∈ wcel 2105 ∩ cin 3961 〈cop 4636 × cxp 5686 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-opab 5210 df-xp 5694 df-rel 5695 |
This theorem is referenced by: xpindi 5846 xpindir 5847 dmxpin 5944 xpssres 6037 xpdisj1 6182 xpdisj2 6183 imainrect 6202 xpima 6203 cnvrescnv 6216 curry1 8127 curry2 8130 fpar 8139 marypha1lem 9470 fpwwe2lem12 10679 hashxplem 14468 sscres 17870 gsumxp 20008 pjfval 21743 pjpm 21745 txbas 23590 txcls 23627 txrest 23654 trust 24253 ressuss 24286 trcfilu 24318 metreslem 24387 ressxms 24553 ressms 24554 mbfmcst 34240 0rrv 34432 poimirlem26 37632 |
Copyright terms: Public domain | W3C validator |