MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnxpss Structured version   Visualization version   GIF version

Theorem rnxpss 6128
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
StepHypRef Expression
1 df-rn 5648 . 2 ran (𝐴 × 𝐵) = dom (𝐴 × 𝐵)
2 cnvxp 6113 . . . 4 (𝐴 × 𝐵) = (𝐵 × 𝐴)
32dmeqi 5864 . . 3 dom (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4 dmxpss 6127 . . 3 dom (𝐵 × 𝐴) ⊆ 𝐵
53, 4eqsstri 3982 . 2 dom (𝐴 × 𝐵) ⊆ 𝐵
61, 5eqsstri 3982 1 ran (𝐴 × 𝐵) ⊆ 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3914   × cxp 5635  ccnv 5636  dom cdm 5637  ran crn 5638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-br 5110  df-opab 5172  df-xp 5643  df-rel 5644  df-cnv 5645  df-dm 5647  df-rn 5648
This theorem is referenced by:  ssxpb  6130  ssrnres  6134  resssxp  6226  funssxp  6701  fconst  6732  dff2  7053  dff3  7054  fliftf  7264  frxp2  8080  frxp3  8087  marypha1lem  9377  marypha1  9378  dfac12lem2  10088  brdom4  10474  nqerf  10874  xptrrel  14874  lern  18488  cnconst2  22657  lmss  22672  tsmsxplem1  23527  causs  24685  i1f0  25074  itg10  25075  taylf  25743  noextendseq  27038  perpln2  27702  gsumpart  31953  locfinref  32486  sitg0  33010  heicant  36163  rntrclfvOAI  41061  rtrclex  41981  trclexi  41984  rtrclexi  41985  cnvtrcl0  41990  rntrcl  41992  brtrclfv2  42091  xphe  42145  rfovcnvf1od  42368
  Copyright terms: Public domain W3C validator