Theorem dmxpss 6167

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 5696	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 6154	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2789	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5903	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5918	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2789	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4395	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 4035	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5926	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 4039	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 17	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3026	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Syntax hints:   = wceq 1542   ≠ wne 2941   ⊆ wss 3947  ∅c0 4321   × cxp 5673  dom cdm 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683  df-dm 5685

This theorem is referenced by:  rnxpss  6168  ssxpb  6170  resssxp  6266  funssxp  6743  dff3  7097  fparlem3  8095  fparlem4  8096  frxp2  8125  frxp3  8132  brdom3  10519  brdom5  10520  brdom4  10521  canthwelem  10641  pwfseqlem4  10653  uzrdgfni  13919  xptrrel  14923  rlimpm  15440  isohom  17719  ledm  18539  gsumxp  19836  dprd2d2  19906  tsmsxp  23641  dvbssntr  25399  gsumpart  32185  esum2d  33029  poimirlem3  36429  rtrclex  42301  trclexi  42304  rtrclexi  42305  cnvtrcl0  42310  dmtrcl  42311  rfovcnvf1od  42688  issmflem  45378  fvconstr  47424  fvconstrn0  47425  fvconstr2  47426  fvconst0ci  47427  fvconstdomi  47428