Theorem dmxpss 6124

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 5644	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 6111	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2780	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5852	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5867	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2780	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4353	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 3982	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5875	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 3996	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 17	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3008	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Syntax hints:   = wceq 1540   ≠ wne 2925   ⊆ wss 3905  ∅c0 4286   × cxp 5621  dom cdm 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631  df-dm 5633

This theorem is referenced by:  rnxpss  6125  ssxpb  6127  resssxp  6222  funssxp  6684  dff3  7038  fparlem3  8054  fparlem4  8055  frxp2  8084  frxp3  8091  brdom3  10441  brdom5  10442  brdom4  10443  canthwelem  10563  pwfseqlem4  10575  uzrdgfni  13883  xptrrel  14905  rlimpm  15425  isohom  17701  ledm  18514  gsumxp  19873  dprd2d2  19943  tsmsxp  24058  dvbssntr  25817  noseqrdgfn  28223  gsumpart  33023  esum2d  34059  poimirlem3  37602  rtrclex  43590  trclexi  43593  rtrclexi  43594  cnvtrcl0  43599  dmtrcl  43600  rfovcnvf1od  43977  issmflem  46709  fvconstr  48847  fvconstrn0  48848  fvconstr2  48849  fvconst0ci  48876  fvconstdomi  48877