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

Theorem inxp 5423
Description: The 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 5421 . . 3 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐷)}) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ (𝑥𝐶𝑦𝐷))}
2 an4 646 . . . . 5 (((𝑥𝐴𝑦𝐵) ∧ (𝑥𝐶𝑦𝐷)) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑦𝐵𝑦𝐷)))
3 elin 3958 . . . . . 6 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elin 3958 . . . . . 6 (𝑦 ∈ (𝐵𝐷) ↔ (𝑦𝐵𝑦𝐷))
53, 4anbi12i 620 . . . . 5 ((𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷)) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑦𝐵𝑦𝐷)))
62, 5bitr4i 269 . . . 4 (((𝑥𝐴𝑦𝐵) ∧ (𝑥𝐶𝑦𝐷)) ↔ (𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷)))
76opabbii 4876 . . 3 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ (𝑥𝐶𝑦𝐷))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷))}
81, 7eqtri 2787 . 2 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐷)}) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷))}
9 df-xp 5283 . . 3 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
10 df-xp 5283 . . 3 (𝐶 × 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐷)}
119, 10ineq12i 3974 . 2 ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)} ∩ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦𝐷)})
12 df-xp 5283 . 2 ((𝐴𝐶) × (𝐵𝐷)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐶) ∧ 𝑦 ∈ (𝐵𝐷))}
138, 11, 123eqtr4i 2797 1 ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴𝐶) × (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1652  wcel 2155  cin 3731  {copab 4871   × cxp 5275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-opab 4872  df-xp 5283  df-rel 5284
This theorem is referenced by:  xpindi  5424  xpindir  5425  dmxpin  5514  xpssres  5608  xpdisj1  5738  xpdisj2  5739  imainrect  5758  xpima  5759  curry1  7471  curry2  7474  fpar  7483  marypha1lem  8546  fpwwe2lem13  9717  hashxplem  13421  sscres  16750  gsumxp  18641  pjfval  20326  pjpm  20328  txbas  21650  txcls  21687  txrest  21714  trust  22312  ressuss  22346  trcfilu  22377  metreslem  22446  ressxms  22609  ressms  22610  mbfmcst  30703  0rrv  30896  poimirlem26  33791
  Copyright terms: Public domain W3C validator