Theorem rnxpss 6128

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 5633	. 2 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6113	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5851	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4		dmxpss 6127	. . 3 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵
5	3, 4	eqsstri 3969	. 2 ⊢ dom ◡(𝐴 × 𝐵) ⊆ 𝐵
6	1, 5	eqsstri 3969	1 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵

Syntax hints:   ⊆ wss 3890   × cxp 5620  ^◡ccnv 5621  dom cdm 5622  ran crn 5623

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-11 2163  ax-ext 2709  ax-sep 5231  ax-pr 5368

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 5628  df-rel 5629  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  ssxpb  6130  ssrnres  6134  resssxp  6226  funssxp  6688  fconst  6718  dff2  7043  dff3  7044  fliftf  7261  frxp2  8085  frxp3  8092  marypha1lem  9337  marypha1  9338  dfac12lem2  10056  brdom4  10441  nqerf  10842  xptrrel  14931  lern  18546  cnconst2  23257  lmss  23272  tsmsxplem1  24127  causs  25274  i1f0  25663  itg10  25664  taylf  26339  noextendseq  27650  perpln2  28798  gsumpart  33144  locfinref  34006  sitg0  34511  heicant  37987  rntrclfvOAI  43134  rtrclex  44059  trclexi  44062  rtrclexi  44063  cnvtrcl0  44068  rntrcl  44070  brtrclfv2  44169  xphe  44223  rfovcnvf1od  44446