Theorem rnxpss 6176

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

Syntax hints:   ⊆ wss 3947   × cxp 5676  ^◡ccnv 5677  dom cdm 5678  ran crn 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-opab 5211  df-xp 5684  df-rel 5685  df-cnv 5686  df-dm 5688  df-rn 5689

This theorem is referenced by:  ssxpb  6178  ssrnres  6182  resssxp  6274  funssxp  6752  fconst  6783  dff2  7109  dff3  7110  fliftf  7323  frxp2  8149  frxp3  8156  marypha1lem  9457  marypha1  9458  dfac12lem2  10168  brdom4  10554  nqerf  10954  xptrrel  14960  lern  18583  cnconst2  23200  lmss  23215  tsmsxplem1  24070  causs  25239  i1f0  25629  itg10  25630  taylf  26308  noextendseq  27613  perpln2  28528  gsumpart  32782  locfinref  33442  sitg0  33966  heicant  37128  rntrclfvOAI  42111  rtrclex  43047  trclexi  43050  rtrclexi  43051  cnvtrcl0  43056  rntrcl  43058  brtrclfv2  43157  xphe  43211  rfovcnvf1od  43434