Theorem dmxpss 6171

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 5684	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 5763	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2814	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5897	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5912	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2814	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4358	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 3982	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5921	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 3996	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 18	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3041	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Syntax hints:   = wceq 1570   ≠ wne 2958   ⊆ wss 3906  ∅c0 4287   × cxp 5661  dom cdm 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-dm 5673

This theorem is referenced by:  rnxpss  6172  ssxpb  6174  resssxp  6273  funssxp  6736  dff3  7097  fparlem3  8110  fparlem4  8111  frxp2  8141  frxp3  8148  brdom3  10513  brdom5  10514  brdom4  10515  canthwelem  10636  pwfseqlem4  10648  uzrdgfni  13996  xptrrel  15019  rlimpm  15553  isohom  17834  ledm  18647  gsumxp  20047  dprd2d2  20117  tsmsxp  24293  dvbssntr  26040  noseqrdgfn  28480  gsumpart  33364  esum2d  34464  poimirlem3  38255  rtrclex  44326  trclexi  44329  rtrclexi  44330  cnvtrcl0  44335  dmtrcl  44336  rfovcnvf1od  44713  issmflem  47424  fvconstr  49623  fvconstrn0  49624  fvconstr2  49625  fvconst0ci  49652  fvconstdomi  49653