Theorem rnxpss 6029

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 5566	. 2 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6014	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5773	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4		dmxpss 6028	. . 3 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵
5	3, 4	eqsstri 4001	. 2 ⊢ dom ◡(𝐴 × 𝐵) ⊆ 𝐵
6	1, 5	eqsstri 4001	1 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵

Syntax hints:   ⊆ wss 3936   × cxp 5553  ^◡ccnv 5554  dom cdm 5555  ran crn 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-rel 5562  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  ssxpb  6031  ssrnres  6035  funssxp  6535  fconst  6565  dff2  6865  dff3  6866  fliftf  7068  marypha1lem  8897  marypha1  8898  dfac12lem2  9570  brdom4  9952  nqerf  10352  xptrrel  14340  lern  17835  cnconst2  21891  lmss  21906  tsmsxplem1  22761  causs  23901  i1f0  24288  itg10  24289  taylf  24949  perpln2  26497  locfinref  31105  sitg0  31604  noextendseq  33174  heicant  34942  rntrclfvOAI  39308  rtrclex  39997  trclexi  40000  rtrclexi  40001  cnvtrcl0  40006  rntrcl  40008  brtrclfv2  40092  rp-imass  40137  xphe  40147  rfovcnvf1od  40370