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

Theorem rnxpss 5288
Description: The range of a Cartesian product is a subclass of the second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
rnxpss  |-  ran  ( A  X.  B )  C_  B

Proof of Theorem rnxpss
StepHypRef Expression
1 df-rn 4864 . 2  |-  ran  ( A  X.  B )  =  dom  `' ( A  X.  B )
2 cnvxp 5273 . . . 4  |-  `' ( A  X.  B )  =  ( B  X.  A )
32dmeqi 5055 . . 3  |-  dom  `' ( A  X.  B
)  =  dom  ( B  X.  A )
4 dmxpss 5287 . . 3  |-  dom  ( B  X.  A )  C_  B
53, 4eqsstri 3494 . 2  |-  dom  `' ( A  X.  B
)  C_  B
61, 5eqsstri 3494 1  |-  ran  ( A  X.  B )  C_  B
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3436    X. cxp 4851   `'ccnv 4852   dom cdm 4853   ran crn 4854
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-rel 4860  df-cnv 4861  df-dm 4863  df-rn 4864
This theorem is referenced by:  ssxpb  5290  ssrnres  5294  funssxp  5759  fconst  5786  dff2  6049  dff3  6050  fliftf  6223  marypha1lem  7956  marypha1  7957  dfac12lem2  8581  brdom4  8965  nqerf  9362  xptrrel  13044  lern  16470  cnconst2  20297  lmss  20312  tsmsxplem1  21165  causs  22266  i1f0  22643  itg10  22644  taylf  23314  perpln2  24754  locfinref  28676  sitg0  29187  heicant  31939  rntrclfvOAI  35502  rtrclex  36194  trclexi  36197  rtrclexi  36198  cnvtrcl0  36203  rntrcl  36205  brtrclfv2  36289  rp-imass  36336  xphe  36346
  Copyright terms: Public domain W3C validator