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

Theorem rnss 5895
Description: Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
rnss (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)

Proof of Theorem rnss
StepHypRef Expression
1 cnvss 5829 . . 3 (𝐴𝐵𝐴𝐵)
2 dmss 5859 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
31, 2syl 17 . 2 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
4 df-rn 5645 . 2 ran 𝐴 = dom 𝐴
5 df-rn 5645 . 2 ran 𝐵 = dom 𝐵
63, 4, 53sstr4g 3990 1 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3911  ccnv 5633  dom cdm 5634  ran crn 5635
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-ext 2704
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-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-cnv 5642  df-dm 5644  df-rn 5645
This theorem is referenced by:  rnssi  5896  imass1  6054  imass2  6055  ssxpb  6127  sofld  6140  resssxp  6223  funssxp  6698  dff2  7050  dff3  7051  fliftf  7261  1stcof  7952  2ndcof  7953  frxp  8059  frxp2  8077  frxp3  8084  fodomfi  9272  marypha1lem  9374  marypha1  9375  dfac12lem2  10085  fpwwe2lem12  10583  prdsvallem  17341  prdsval  17342  prdsbas  17344  prdsplusg  17345  prdsmulr  17346  prdsvsca  17347  prdshom  17354  catcfuccl  18010  catcfucclOLD  18011  catcxpccl  18100  catcxpcclOLD  18101  odf1o2  19360  dprdres  19812  lmss  22665  txss12  22972  txbasval  22973  fmss  23313  tsmsxplem1  23520  ustimasn  23596  utopbas  23603  metustexhalf  23928  causs  24678  ovoliunlem1  24882  dvcnvrelem1  25397  taylf  25736  subgrprop3  28266  sspba  29711  imadifxp  31565  gsumpart  31946  metideq  32531  sxbrsigalem5  32945  omsmon  32955  carsggect  32975  carsgclctunlem2  32976  heicant  36159  mblfinlem1  36161  symrefref2  37071  dicval  39685  rntrclfvOAI  41057  diophrw  41125  dnnumch2  41415  lmhmlnmsplit  41457  hbtlem6  41499  mptrcllem  41973  rntrcl  41988  dfrcl2  42034  relexpss1d  42065  rfovcnvf1od  42364  supcnvlimsup  44067  fourierdlem42  44476  sge0less  44719
  Copyright terms: Public domain W3C validator