Theorem dmxpss 6129

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 5645	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
2		xp0 5724	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
3	1, 2	eqtrdi 2787	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5854	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5869	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2787	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4352	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 3978	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5878	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 3992	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 17	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3015	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Syntax hints:   = wceq 1541   ≠ wne 2932   ⊆ wss 3901  ∅c0 4285   × cxp 5622  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-dm 5634

This theorem is referenced by:  rnxpss  6130  ssxpb  6132  resssxp  6228  funssxp  6690  dff3  7045  fparlem3  8056  fparlem4  8057  frxp2  8086  frxp3  8093  brdom3  10438  brdom5  10439  brdom4  10440  canthwelem  10561  pwfseqlem4  10573  uzrdgfni  13881  xptrrel  14903  rlimpm  15423  isohom  17700  ledm  18513  gsumxp  19905  dprd2d2  19975  tsmsxp  24099  dvbssntr  25857  noseqrdgfn  28302  gsumpart  33146  esum2d  34250  poimirlem3  37820  rtrclex  43854  trclexi  43857  rtrclexi  43858  cnvtrcl0  43863  dmtrcl  43864  rfovcnvf1od  44241  issmflem  46967  fvconstr  49103  fvconstrn0  49104  fvconstr2  49105  fvconst0ci  49132  fvconstdomi  49133