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

Theorem dmxp 5686
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 5454 . . 3 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
21dmeqi 5664 . 2 dom (𝐴 × 𝐵) = dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
3 n0 4234 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑥 𝑥𝐵)
43biimpi 217 . . . 4 (𝐵 ≠ ∅ → ∃𝑥 𝑥𝐵)
54ralrimivw 3150 . . 3 (𝐵 ≠ ∅ → ∀𝑦𝐴𝑥 𝑥𝐵)
6 dmopab3 5679 . . 3 (∀𝑦𝐴𝑥 𝑥𝐵 ↔ dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
75, 6sylib 219 . 2 (𝐵 ≠ ∅ → dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
82, 7syl5eq 2843 1 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wex 1761  wcel 2081  wne 2984  wral 3105  c0 4215  {copab 5028   × cxp 5446  dom cdm 5448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pr 5226
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rab 3114  df-v 3439  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-br 4967  df-opab 5029  df-xp 5454  df-dm 5458
This theorem is referenced by:  dmxpid  5687  rnxp  5908  dmxpss  5909  ssxpb  5912  relrelss  6004  unixp  6013  xpexr2  7485  xpexcnv  7486  frxp  7678  mpocurryd  7791  fodomr  8520  nqerf  10203  dmtrclfv  14217  pwsbas  16594  pwsle  16599  imasaddfnlem  16635  imasvscafn  16644  efgrcl  18573  frlmip  20609  txindislem  21930  metustexhalf  22854  rrxip  23681  dveq0  24285  dv11cn  24286  mbfmcst  31139  eulerpartlemt  31251  0rrv  31331  noxp1o  32786  noextendseq  32790  bdayfo  32798  noetalem3  32835  noetalem4  32836  curf  34427  curunc  34431  ismgmOLD  34686  diophrw  38867
  Copyright terms: Public domain W3C validator