Theorem rnxpss 6163

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

This proof depends on syntax axioms:   ⊆ wss 3895   × cxp 5648  ^◡ccnv 5649  dom cdm 5650  ran crn 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  ssxpb  6165  ssrnres  6169  resssxp  6272  funssxp  6738  fconst  6768  dff2  7099  dff3  7100  fliftf  7323  frxp2  8161  frxp3  8168  marypha1lem  9426  marypha1  9427  dfac12lem2  10224  brdom4  10610  nqerf  11016  xptrrel  15134  lern  18766  cnconst2  23602  lmss  23617  tsmsxplem1  24473  causs  25620  i1f0  26009  itg10  26010  taylf  26689  noextendseq  28025  perpln2  29187  gsumpart  33667  locfinref  34516  sitg0  35021  heicant  38649  rntrclfvOAI  43778  rtrclex  44693  trclexi  44696  rtrclexi  44697  cnvtrcl0  44702  rntrcl  44704  brtrclfv2  44803  xphe  44857  rfovcnvf1od  45080  rnhfstructsshf  46103