Theorem dmxpss 6193

Description: The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007.)

Assertion

Ref	Expression
dmxpss	⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Proof of Theorem dmxpss

Step	Hyp	Ref	Expression
1		xpeq2 5710	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 6180	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2791	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5919	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5934	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2791	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4406	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 4050	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5942	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 4054	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 17	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3023	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Syntax hints:   = wceq 1537   ≠ wne 2938   ⊆ wss 3963  ∅c0 4339   × cxp 5687  dom cdm 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697  df-dm 5699

This theorem is referenced by:  rnxpss  6194  ssxpb  6196  resssxp  6292  funssxp  6765  dff3  7120  fparlem3  8138  fparlem4  8139  frxp2  8168  frxp3  8175  brdom3  10566  brdom5  10567  brdom4  10568  canthwelem  10688  pwfseqlem4  10700  uzrdgfni  13996  xptrrel  15016  rlimpm  15533  isohom  17824  ledm  18648  gsumxp  20009  dprd2d2  20079  tsmsxp  24179  dvbssntr  25950  noseqrdgfn  28327  gsumpart  33043  esum2d  34074  poimirlem3  37610  rtrclex  43607  trclexi  43610  rtrclexi  43611  cnvtrcl0  43616  dmtrcl  43617  rfovcnvf1od  43994  issmflem  46683  fvconstr  48686  fvconstrn0  48687  fvconstr2  48688  fvconst0ci  48689  fvconstdomi  48690