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

Theorem rnss 5803
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 5737 . . 3 (𝐴𝐵𝐴𝐵)
2 dmss 5765 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
31, 2syl 17 . 2 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
4 df-rn 5560 . 2 ran 𝐴 = dom 𝐴
5 df-rn 5560 . 2 ran 𝐵 = dom 𝐵
63, 4, 53sstr4g 4011 1 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3935  ccnv 5548  dom cdm 5549  ran crn 5550
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 2793
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-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-cnv 5557  df-dm 5559  df-rn 5560
This theorem is referenced by:  rnssi  5804  imass1  5958  imass2  5959  ssxpb  6025  sofld  6038  funssxp  6529  dff2  6858  dff3  6859  fliftf  7057  1stcof  7710  2ndcof  7711  frxp  7811  fodomfi  8786  marypha1lem  8886  marypha1  8887  dfac12lem2  9559  fpwwe2lem13  10053  prdsval  16718  prdsbas  16720  prdsplusg  16721  prdsmulr  16722  prdsvsca  16723  prdshom  16730  catcfuccl  17359  catcxpccl  17447  odf1o2  18629  dprdres  19081  lmss  21836  txss12  22143  txbasval  22144  fmss  22484  tsmsxplem1  22690  ustimasn  22766  utopbas  22773  metustexhalf  23095  causs  23830  ovoliunlem1  24032  dvcnvrelem1  24543  taylf  24878  subgrprop3  26986  sspba  28432  imadifxp  30280  metideq  31033  sxbrsigalem5  31446  omsmon  31456  carsggect  31476  carsgclctunlem2  31477  heicant  34809  mblfinlem1  34811  symrefref2  35681  dicval  38194  rntrclfvOAI  39168  diophrw  39236  dnnumch2  39525  lmhmlnmsplit  39567  hbtlem6  39609  mptrcllem  39853  rntrcl  39868  dfrcl2  39899  relexpss1d  39930  rp-imass  39997  rfovcnvf1od  40230  supcnvlimsup  41901  fourierdlem42  42315  sge0less  42555
  Copyright terms: Public domain W3C validator