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

Theorem dmxp 5552
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 5324 . . 3 (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
21dmeqi 5533 . 2 dom (𝐴 × 𝐵) = dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)}
3 n0 4139 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑥 𝑥𝐵)
43biimpi 207 . . . 4 (𝐵 ≠ ∅ → ∃𝑥 𝑥𝐵)
54ralrimivw 3162 . . 3 (𝐵 ≠ ∅ → ∀𝑦𝐴𝑥 𝑥𝐵)
6 dmopab3 5545 . . 3 (∀𝑦𝐴𝑥 𝑥𝐵 ↔ dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
75, 6sylib 209 . 2 (𝐵 ≠ ∅ → dom {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐴𝑥𝐵)} = 𝐴)
82, 7syl5eq 2859 1 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wex 1859  wcel 2157  wne 2985  wral 3103  c0 4123  {copab 4913   × cxp 5316  dom cdm 5318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-br 4852  df-opab 4914  df-xp 5324  df-dm 5328
This theorem is referenced by:  dmxpid  5553  rnxp  5782  dmxpss  5783  ssxpb  5786  relrelss  5880  unixp  5889  xpexr2  7340  xpexcnv  7341  frxp  7524  mpt2curryd  7633  fodomr  8353  nqerf  10040  dmtrclfv  13985  pwsbas  16355  pwsle  16360  imasaddfnlem  16396  imasvscafn  16405  efgrcl  18332  frlmip  20331  txindislem  21654  metustexhalf  22578  rrxip  23396  dveq0  23983  dv11cn  23984  mbfmcst  30652  eulerpartlemt  30764  0rrv  30844  noxp1o  32142  noextendseq  32146  bdayfo  32154  noetalem3  32191  noetalem4  32192  curf  33702  curunc  33706  ismgmOLD  33962  diophrw  37825
  Copyright terms: Public domain W3C validator