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

Theorem dmxp 5885
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 5640 . . 3 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
21dmeqi 5861 . 2 dom (𝐴 × 𝐵) = dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
3 n0 4307 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑥 𝑥𝐵)
43biimpi 215 . . . 4 (𝐵 ≠ ∅ → ∃𝑥 𝑥𝐵)
54ralrimivw 3144 . . 3 (𝐵 ≠ ∅ → ∀𝑦𝐴𝑥 𝑥𝐵)
6 dmopab3 5876 . . 3 (∀𝑦𝐴𝑥 𝑥𝐵 ↔ dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
75, 6sylib 217 . 2 (𝐵 ≠ ∅ → dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
82, 7eqtrid 2785 1 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wex 1782  wcel 2107  wne 2940  wral 3061  c0 4283  {copab 5168   × cxp 5632  dom cdm 5634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-dm 5644
This theorem is referenced by:  dmxpid  5886  rnxp  6123  dmxpss  6124  ssxpb  6127  relrelss  6226  unixp  6235  xpexr2  7857  xpexcnv  7858  frxp  8059  mpocurryd  8201  fodomr  9075  nqerf  10871  dmtrclfv  14909  pwsbas  17374  pwsle  17379  imasaddfnlem  17415  imasvscafn  17424  efgrcl  19502  frlmip  21200  txindislem  23000  metustexhalf  23928  rrxip  24770  dveq0  25380  dv11cn  25381  noxp1o  27027  noextendseq  27031  bdayfo  27041  noetasuplem2  27098  noetasuplem4  27100  noetainflem2  27102  noetainflem4  27104  mbfmcst  32916  eulerpartlemt  33028  0rrv  33108  curf  36102  curunc  36106  ismgmOLD  36355  diophrw  41125  onnog  41789  onnobdayg  41790  bdaybndbday  41792
  Copyright terms: Public domain W3C validator