Theorem dmxpss 6162

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 5671	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 5750	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2811	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5886	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5901	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2811	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4349	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 3952	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5910	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 3966	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 18	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3038	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

This proof depends on syntax axioms:   = wceq 1569   ≠ wne 2955   ⊆ wss 3895  ∅c0 4278   × cxp 5648  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-dm 5660

This theorem is used by:  rnxpss  6163  ssxpb  6165  resssxp  6272  funssxp  6739  dff3  7101  fparlem3  8128  fparlem4  8129  frxp2  8164  frxp3  8171  brdom3  10611  brdom5  10612  brdom4  10613  canthwelem  10739  pwfseqlem4  10751  uzrdgfni  14105  xptrrel  15139  rlimpm  15673  isohom  17957  ledm  18770  gsumxp  20196  dprd2d2  20266  tsmsxp  24480  dvbssntr  26226  noseqrdgfn  28698  gsumpart  33671  esum2d  34772  poimirlem3  38635  rtrclex  44711  trclexi  44714  rtrclexi  44715  cnvtrcl0  44720  dmtrcl  44721  rfovcnvf1od  45098  issmflem  47831  ovconstbrd  50067  ovconstbrn0d  50068  elovconstbrd  50069  fvconst0ci  50099  fvconstdomi  50100