Theorem rnxpss 6130

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 5636	. 2 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6115	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5853	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4		dmxpss 6129	. . 3 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵
5	3, 4	eqsstri 3968	. 2 ⊢ dom ◡(𝐴 × 𝐵) ⊆ 𝐵
6	1, 5	eqsstri 3968	1 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵

Syntax hints:   ⊆ wss 3890   × cxp 5623  ^◡ccnv 5624  dom cdm 5625  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-11 2168  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  ssxpb  6132  ssrnres  6136  resssxp  6228  funssxp  6690  fconst  6720  dff2  7047  dff3  7048  fliftf  7266  frxp2  8091  frxp3  8098  marypha1lem  9343  marypha1  9344  dfac12lem2  10065  brdom4  10450  nqerf  10851  xptrrel  14940  lern  18555  cnconst2  23273  lmss  23288  tsmsxplem1  24143  causs  25290  i1f0  25679  itg10  25680  taylf  26351  noextendseq  27656  perpln2  28804  gsumpart  33151  locfinref  34032  sitg0  34537  heicant  38023  rntrclfvOAI  43141  rtrclex  44062  trclexi  44065  rtrclexi  44066  cnvtrcl0  44071  rntrcl  44073  brtrclfv2  44172  xphe  44226  rfovcnvf1od  44449