Theorem rnxpss 6162

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 5663	. 2 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6146	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5885	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4		dmxpss 6161	. . 3 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵
5	3, 4	eqsstri 3985	. 2 ⊢ dom ◡(𝐴 × 𝐵) ⊆ 𝐵
6	1, 5	eqsstri 3985	1 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵

Syntax hints:   ⊆ wss 3907   × cxp 5650  ^◡ccnv 5651  dom cdm 5652  ran crn 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658  df-rel 5659  df-cnv 5660  df-dm 5662  df-rn 5663

This theorem is referenced by:  ssxpb  6164  ssrnres  6168  resssxp  6261  funssxp  6724  fconst  6754  dff2  7084  dff3  7085  fliftf  7303  frxp2  8128  frxp3  8135  marypha1lem  9381  marypha1  9382  dfac12lem2  10116  brdom4  10502  nqerf  10903  xptrrel  15007  lern  18637  cnconst2  23401  lmss  23416  tsmsxplem1  24271  causs  25418  i1f0  25807  itg10  25808  taylf  26482  noextendseq  27789  perpln2  28942  gsumpart  33296  locfinref  34148  sitg0  34653  heicant  38166  rntrclfvOAI  43284  rtrclex  44205  trclexi  44208  rtrclexi  44209  cnvtrcl0  44214  rntrcl  44216  brtrclfv2  44315  xphe  44369  rfovcnvf1od  44592