Theorem rnxpss 6147

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

Syntax hints:   ⊆ wss 3899   × cxp 5638  ^◡ccnv 5639  dom cdm 5640  ran crn 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-11 2185  ax-ext 2728  ax-sep 5240  ax-pr 5384

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-opab 5157  df-xp 5646  df-rel 5647  df-cnv 5648  df-dm 5650  df-rn 5651

This theorem is referenced by:  ssxpb  6149  ssrnres  6153  resssxp  6246  funssxp  6709  fconst  6739  dff2  7069  dff3  7070  fliftf  7288  frxp2  8112  frxp3  8119  marypha1lem  9369  marypha1  9370  dfac12lem2  10091  brdom4  10477  nqerf  10878  xptrrel  14983  lern  18599  cnconst2  23316  lmss  23331  tsmsxplem1  24186  causs  25333  i1f0  25722  itg10  25723  taylf  26394  noextendseq  27701  perpln2  28850  gsumpart  33197  locfinref  34092  sitg0  34597  heicant  38102  rntrclfvOAI  43220  rtrclex  44141  trclexi  44144  rtrclexi  44145  cnvtrcl0  44150  rntrcl  44152  brtrclfv2  44251  xphe  44305  rfovcnvf1od  44528