Theorem rnxpss 6145

Description: The range of a Cartesian product is included in its second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
rnxpss	⊢ ran (𝐴 × 𝐵) ⊆ 𝐵

Proof of Theorem rnxpss

Step	Hyp	Ref	Expression
1		df-rn 5649	. 2 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6130	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5868	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4		dmxpss 6144	. . 3 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵
5	3, 4	eqsstri 3993	. 2 ⊢ dom ◡(𝐴 × 𝐵) ⊆ 𝐵
6	1, 5	eqsstri 3993	1 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵

Syntax hints:   ⊆ wss 3914   × cxp 5636  ^◡ccnv 5637  dom cdm 5638  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  ssxpb  6147  ssrnres  6151  resssxp  6243  funssxp  6716  fconst  6746  dff2  7071  dff3  7072  fliftf  7290  frxp2  8123  frxp3  8130  marypha1lem  9384  marypha1  9385  dfac12lem2  10098  brdom4  10483  nqerf  10883  xptrrel  14946  lern  18550  cnconst2  23170  lmss  23185  tsmsxplem1  24040  causs  25198  i1f0  25588  itg10  25589  taylf  26268  noextendseq  27579  perpln2  28638  gsumpart  32997  locfinref  33831  sitg0  34337  heicant  37649  rntrclfvOAI  42679  rtrclex  43606  trclexi  43609  rtrclexi  43610  cnvtrcl0  43615  rntrcl  43617  brtrclfv2  43716  xphe  43770  rfovcnvf1od  43993