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

Theorem rnxpss 6022
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 5559 . 2 ran (𝐴 × 𝐵) = dom (𝐴 × 𝐵)
2 cnvxp 6007 . . . 4 (𝐴 × 𝐵) = (𝐵 × 𝐴)
32dmeqi 5766 . . 3 dom (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4 dmxpss 6021 . . 3 dom (𝐵 × 𝐴) ⊆ 𝐵
53, 4eqsstri 3998 . 2 dom (𝐴 × 𝐵) ⊆ 𝐵
61, 5eqsstri 3998 1 ran (𝐴 × 𝐵) ⊆ 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3933   × cxp 5546  ccnv 5547  dom cdm 5548  ran crn 5549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-cnv 5556  df-dm 5558  df-rn 5559
This theorem is referenced by:  ssxpb  6024  ssrnres  6028  funssxp  6528  fconst  6558  dff2  6857  dff3  6858  fliftf  7057  marypha1lem  8885  marypha1  8886  dfac12lem2  9558  brdom4  9940  nqerf  10340  xptrrel  14328  lern  17823  cnconst2  21819  lmss  21834  tsmsxplem1  22688  causs  23828  i1f0  24215  itg10  24216  taylf  24876  perpln2  26424  locfinref  31004  sitg0  31503  noextendseq  33071  heicant  34808  rntrclfvOAI  39166  rtrclex  39855  trclexi  39858  rtrclexi  39859  cnvtrcl0  39864  rntrcl  39866  brtrclfv2  39950  rp-imass  39995  xphe  40005  rfovcnvf1od  40228
  Copyright terms: Public domain W3C validator