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

Theorem dmxpss 5747
Description: The domain of a Cartesian product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.)
Assertion
Ref Expression
dmxpss dom (𝐴 × 𝐵) ⊆ 𝐴

Proof of Theorem dmxpss
StepHypRef Expression
1 xpeq2 5297 . . . . . 6 (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2 xp0 5734 . . . . . 6 (𝐴 × ∅) = ∅
31, 2syl6eq 2814 . . . . 5 (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
43dmeqd 5493 . . . 4 (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5 dm0 5506 . . . 4 dom ∅ = ∅
64, 5syl6eq 2814 . . 3 (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7 0ss 4133 . . 3 ∅ ⊆ 𝐴
86, 7syl6eqss 3814 . 2 (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9 dmxp 5511 . . 3 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10 eqimss 3816 . . 3 (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
119, 10syl 17 . 2 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
128, 11pm2.61ine 3019 1 dom (𝐴 × 𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  wne 2936  wss 3731  c0 4078   × cxp 5274  dom cdm 5276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pr 5061
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rab 3063  df-v 3351  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-sn 4334  df-pr 4336  df-op 4340  df-br 4809  df-opab 4871  df-xp 5282  df-rel 5283  df-cnv 5284  df-dm 5286
This theorem is referenced by:  rnxpss  5748  ssxpb  5750  funssxp  6242  dff3  6561  fparlem3  7480  fparlem4  7481  brdom3  9602  brdom5  9603  brdom4  9604  canthwelem  9724  pwfseqlem4  9736  uzrdgfni  12964  xptrrel  14007  rlimpm  14517  xpsc0  16487  xpsc1  16488  xpsfrnel2  16492  isohom  16702  ledm  17491  gsumxp  18640  dprd2d2  18709  tsmsxp  22236  dvbssntr  23954  esum2d  30536  poimirlem3  33768  rtrclex  38531  trclexi  38534  rtrclexi  38535  cnvtrcl0  38540  dmtrcl  38541  rp-imass  38671  rfovcnvf1od  38904  issmflem  41508
  Copyright terms: Public domain W3C validator