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 2788	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
4	3	dmeqd 5854	. . . 4 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = dom ∅)
5		dm0 5869	. . . 4 ⊢ dom ∅ = ∅
6	4, 5	eqtrdi 2788	. . 3 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) = ∅)
7		0ss 4341	. . 3 ⊢ ∅ ⊆ 𝐴
8	6, 7	eqsstrdi 3967	. 2 ⊢ (𝐵 = ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
9		dmxp 5878	. . 3 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
10		eqimss 3981	. . 3 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → dom (𝐴 × 𝐵) ⊆ 𝐴)
11	9, 10	syl 17	. 2 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) ⊆ 𝐴)
12	8, 11	pm2.61ine 3016	1 ⊢ dom (𝐴 × 𝐵) ⊆ 𝐴

Syntax hints:   = wceq 1542   ≠ wne 2933   ⊆ wss 3890  ∅c0 4274   × 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-dm 5634

This theorem is referenced by:  rnxpss  6130  ssxpb  6132  resssxp  6228  funssxp  6690  dff3  7046  fparlem3  8057  fparlem4  8058  frxp2  8087  frxp3  8094  brdom3  10441  brdom5  10442  brdom4  10443  canthwelem  10564  pwfseqlem4  10576  uzrdgfni  13911  xptrrel  14933  rlimpm  15453  isohom  17734  ledm  18547  gsumxp  19942  dprd2d2  20012  tsmsxp  24130  dvbssntr  25877  noseqrdgfn  28312  gsumpart  33139  esum2d  34253  poimirlem3  37958  rtrclex  44062  trclexi  44065  rtrclexi  44066  cnvtrcl0  44071  dmtrcl  44072  rfovcnvf1od  44449  issmflem  47173  fvconstr  49349  fvconstrn0  49350  fvconstr2  49351  fvconst0ci  49378  fvconstdomi  49379