Theorem rnxpss 6138

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 5643	. 2 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6123	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5861	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4		dmxpss 6137	. . 3 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵
5	3, 4	eqsstri 3982	. 2 ⊢ dom ◡(𝐴 × 𝐵) ⊆ 𝐵
6	1, 5	eqsstri 3982	1 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵

Syntax hints:   ⊆ wss 3903   × cxp 5630  ^◡ccnv 5631  dom cdm 5632  ran crn 5633

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  ssxpb  6140  ssrnres  6144  resssxp  6236  funssxp  6698  fconst  6728  dff2  7053  dff3  7054  fliftf  7271  frxp2  8096  frxp3  8103  marypha1lem  9348  marypha1  9349  dfac12lem2  10067  brdom4  10452  nqerf  10853  xptrrel  14915  lern  18526  cnconst2  23239  lmss  23254  tsmsxplem1  24109  causs  25266  i1f0  25656  itg10  25657  taylf  26336  noextendseq  27647  perpln2  28795  gsumpart  33156  locfinref  34018  sitg0  34523  heicant  37895  rntrclfvOAI  43037  rtrclex  43962  trclexi  43965  rtrclexi  43966  cnvtrcl0  43971  rntrcl  43973  brtrclfv2  44072  xphe  44126  rfovcnvf1od  44349