Theorem rnxpss 5996

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 5530	. 2 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 5981	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5737	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4		dmxpss 5995	. . 3 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵
5	3, 4	eqsstri 3949	. 2 ⊢ dom ◡(𝐴 × 𝐵) ⊆ 𝐵
6	1, 5	eqsstri 3949	1 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵

Syntax hints:   ⊆ wss 3881   × cxp 5517  ^◡ccnv 5518  dom cdm 5519  ran crn 5520

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-rel 5526  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  ssxpb  5998  ssrnres  6002  resssxp  6089  funssxp  6509  fconst  6539  dff2  6842  dff3  6843  fliftf  7047  marypha1lem  8881  marypha1  8882  dfac12lem2  9555  brdom4  9941  nqerf  10341  xptrrel  14331  lern  17827  cnconst2  21888  lmss  21903  tsmsxplem1  22758  causs  23902  i1f0  24291  itg10  24292  taylf  24956  perpln2  26505  gsumpart  30740  locfinref  31194  sitg0  31714  noextendseq  33287  heicant  35092  rntrclfvOAI  39632  rtrclex  40317  trclexi  40320  rtrclexi  40321  cnvtrcl0  40326  rntrcl  40328  brtrclfv2  40428  xphe  40482  rfovcnvf1od  40705