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

This proof depends on syntax axioms:   ⊆ wss 3900   × cxp 5653  ^◡ccnv 5654  dom cdm 5655  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  ssxpb  6178  ssrnres  6182  resssxp  6290  funssxp  6760  fconst  6790  dff2  7123  dff3  7124  fliftf  7346  frxp2  8188  frxp3  8195  marypha1lem  9452  marypha1  9453  dfac12lem2  10250  brdom4  10636  nqerf  11042  xptrrel  15162  lern  18794  cnconst2  23631  lmss  23646  tsmsxplem1  24502  causs  25649  i1f0  26038  itg10  26039  taylf  26718  noextendseq  28054  perpln2  29216  gsumpart  33694  locfinref  34543  sitg0  35048  heicant  38765  rntrclfvOAI  43895  rtrclex  44809  trclexi  44812  rtrclexi  44813  cnvtrcl0  44818  rntrcl  44820  brtrclfv2  44919  xphe  44973  rfovcnvf1od  45196  rnhfstructsshf  46225