Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  inxp Structured version   Visualization version   GIF version

Theorem inxp 5677
 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.)
Assertion
Ref Expression
inxp ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴𝐶) × (𝐵𝐷))

Proof of Theorem inxp
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inopab 5675 . . 3 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐷)}) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ (𝑥𝐶𝑦𝐷))}
2 an4 655 . . . . 5 (((𝑥𝐴𝑦𝐵) ∧ (𝑥𝐶𝑦𝐷)) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑦𝐵𝑦𝐷)))
3 elin 3876 . . . . . 6 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elin 3876 . . . . . 6 (𝑦 ∈ (𝐵𝐷) ↔ (𝑦𝐵𝑦𝐷))
53, 4anbi12i 629 . . . . 5 ((𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷)) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑦𝐵𝑦𝐷)))
62, 5bitr4i 281 . . . 4 (((𝑥𝐴𝑦𝐵) ∧ (𝑥𝐶𝑦𝐷)) ↔ (𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷)))
76opabbii 5102 . . 3 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ (𝑥𝐶𝑦𝐷))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷))}
81, 7eqtri 2781 . 2 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐷)}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷))}
9 df-xp 5533 . . 3 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
10 df-xp 5533 . . 3 (𝐶 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐷)}
119, 10ineq12i 4117 . 2 ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐷)})
12 df-xp 5533 . 2 ((𝐴𝐶) × (𝐵𝐷)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷))}
138, 11, 123eqtr4i 2791 1 ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴𝐶) × (𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∩ cin 3859  {copab 5097   × cxp 5525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5098  df-xp 5533  df-rel 5534 This theorem is referenced by:  xpindi  5678  xpindir  5679  dmxpin  5776  xpssres  5864  xpdisj1  5994  xpdisj2  5995  imainrect  6014  xpima  6015  cnvrescnv  6028  curry1  7809  curry2  7812  fpar  7821  marypha1lem  8935  fpwwe2lem12  10107  hashxplem  13849  sscres  17157  gsumxp  19169  pjfval  20476  pjpm  20478  txbas  22272  txcls  22309  txrest  22336  trust  22935  ressuss  22969  trcfilu  23000  metreslem  23069  ressxms  23232  ressms  23233  mbfmcst  31749  0rrv  31941  poimirlem26  35389
 Copyright terms: Public domain W3C validator