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

Theorem dmxp 5763
 Description: The domain of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
dmxp (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)

Proof of Theorem dmxp
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-xp 5525 . . 3 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
21dmeqi 5737 . 2 dom (𝐴 × 𝐵) = dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
3 n0 4260 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑥 𝑥𝐵)
43biimpi 219 . . . 4 (𝐵 ≠ ∅ → ∃𝑥 𝑥𝐵)
54ralrimivw 3150 . . 3 (𝐵 ≠ ∅ → ∀𝑦𝐴𝑥 𝑥𝐵)
6 dmopab3 5752 . . 3 (∀𝑦𝐴𝑥 𝑥𝐵 ↔ dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
75, 6sylib 221 . 2 (𝐵 ≠ ∅ → dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
82, 7syl5eq 2845 1 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∅c0 4243  {copab 5092   × cxp 5517  dom cdm 5519 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-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-dm 5529 This theorem is referenced by:  dmxpid  5764  rnxp  5994  dmxpss  5995  ssxpb  5998  relrelss  6092  unixp  6101  xpexr2  7606  xpexcnv  7607  frxp  7803  mpocurryd  7918  fodomr  8652  nqerf  10341  dmtrclfv  14369  pwsbas  16752  pwsle  16757  imasaddfnlem  16793  imasvscafn  16802  efgrcl  18833  frlmip  20467  txindislem  22238  metustexhalf  23163  rrxip  23994  dveq0  24603  dv11cn  24604  mbfmcst  31627  eulerpartlemt  31739  0rrv  31819  noxp1o  33283  noextendseq  33287  bdayfo  33295  noetalem3  33332  noetalem4  33333  curf  35035  curunc  35039  ismgmOLD  35288  diophrw  39698
 Copyright terms: Public domain W3C validator