Theorem rnxpss 6127

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-11 2162  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-rel 5628  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  ssxpb  6129  ssrnres  6133  resssxp  6225  funssxp  6687  fconst  6717  dff2  7041  dff3  7042  fliftf  7258  frxp2  8083  frxp3  8090  marypha1lem  9327  marypha1  9328  dfac12lem2  10046  brdom4  10431  nqerf  10831  xptrrel  14897  lern  18507  cnconst2  23208  lmss  23223  tsmsxplem1  24078  causs  25235  i1f0  25625  itg10  25626  taylf  26305  noextendseq  27616  perpln2  28699  gsumpart  33048  locfinref  33865  sitg0  34370  heicant  37705  rntrclfvOAI  42798  rtrclex  43724  trclexi  43727  rtrclexi  43728  cnvtrcl0  43733  rntrcl  43735  brtrclfv2  43834  xphe  43888  rfovcnvf1od  44111