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

Theorem dmxp 5376
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 5149 . . 3 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
21dmeqi 5357 . 2 dom (𝐴 × 𝐵) = dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
3 n0 3964 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑥 𝑥𝐵)
43biimpi 206 . . . 4 (𝐵 ≠ ∅ → ∃𝑥 𝑥𝐵)
54ralrimivw 2996 . . 3 (𝐵 ≠ ∅ → ∀𝑦𝐴𝑥 𝑥𝐵)
6 dmopab3 5369 . . 3 (∀𝑦𝐴𝑥 𝑥𝐵 ↔ dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
75, 6sylib 208 . 2 (𝐵 ≠ ∅ → dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
82, 7syl5eq 2697 1 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  c0 3948  {copab 4745   × cxp 5141  dom cdm 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-dm 5153
This theorem is referenced by:  dmxpid  5377  rnxp  5599  dmxpss  5600  ssxpb  5603  relrelss  5697  unixp  5706  xpexr2  7149  xpexcnv  7150  frxp  7332  mpt2curryd  7440  fodomr  8152  nqerf  9790  dmtrclfv  13803  pwsbas  16194  pwsle  16199  imasaddfnlem  16235  imasvscafn  16244  efgrcl  18174  frlmip  20165  txindislem  21484  metustexhalf  22408  rrxip  23224  dveq0  23808  dv11cn  23809  mbfmcst  30449  eulerpartlemt  30561  0rrv  30641  noxp1o  31941  noextendseq  31945  bdayfo  31953  noetalem3  31990  noetalem4  31991  curf  33517  curunc  33521  ismgmOLD  33779  diophrw  37639
  Copyright terms: Public domain W3C validator