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 5672	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 5751	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2812	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5887	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5902	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2812	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4350	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 3975	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5911	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 3989	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 18	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3039	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

This proof depends on syntax axioms:   = wceq 1570   ≠ wne 2956   ⊆ wss 3899  ∅c0 4279   × cxp 5649  dom cdm 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-dm 5661

This theorem is used by:  rnxpss  6163  ssxpb  6165  resssxp  6265  funssxp  6730  dff3  7092  fparlem3  8114  fparlem4  8115  frxp2  8145  frxp3  8152  brdom3  10588  brdom5  10589  brdom4  10590  canthwelem  10716  pwfseqlem4  10728  uzrdgfni  14081  xptrrel  15113  rlimpm  15647  isohom  17931  ledm  18744  gsumxp  20170  dprd2d2  20240  tsmsxp  24454  dvbssntr  26200  noseqrdgfn  28674  gsumpart  33606  esum2d  34707  poimirlem3  38509  rtrclex  44576  trclexi  44579  rtrclexi  44580  cnvtrcl0  44585  dmtrcl  44586  rfovcnvf1od  44963  issmflem  47681  ovconstbrd  49916  ovconstbrn0d  49917  elovconstbrd  49918  fvconst0ci  49943  fvconstdomi  49944