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

Theorem rnss 5848
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 5781 . . 3 (𝐴𝐵𝐴𝐵)
2 dmss 5811 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
31, 2syl 17 . 2 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
4 df-rn 5600 . 2 ran 𝐴 = dom 𝐴
5 df-rn 5600 . 2 ran 𝐵 = dom 𝐵
63, 4, 53sstr4g 3966 1 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3887  ccnv 5588  dom cdm 5589  ran crn 5590
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-cnv 5597  df-dm 5599  df-rn 5600
This theorem is referenced by:  rnssi  5849  imass1  6009  imass2  6010  ssxpb  6077  sofld  6090  resssxp  6173  funssxp  6629  dff2  6975  dff3  6976  fliftf  7186  1stcof  7861  2ndcof  7862  frxp  7967  fodomfi  9092  marypha1lem  9192  marypha1  9193  dfac12lem2  9900  fpwwe2lem12  10398  prdsvallem  17165  prdsval  17166  prdsbas  17168  prdsplusg  17169  prdsmulr  17170  prdsvsca  17171  prdshom  17178  catcfuccl  17834  catcfucclOLD  17835  catcxpccl  17924  catcxpcclOLD  17925  odf1o2  19178  dprdres  19631  lmss  22449  txss12  22756  txbasval  22757  fmss  23097  tsmsxplem1  23304  ustimasn  23380  utopbas  23387  metustexhalf  23712  causs  24462  ovoliunlem1  24666  dvcnvrelem1  25181  taylf  25520  subgrprop3  27643  sspba  29089  imadifxp  30940  gsumpart  31315  metideq  31843  sxbrsigalem5  32255  omsmon  32265  carsggect  32285  carsgclctunlem2  32286  frxp2  33791  frxp3  33797  heicant  35812  mblfinlem1  35814  symrefref2  36677  dicval  39190  rntrclfvOAI  40513  diophrw  40581  dnnumch2  40870  lmhmlnmsplit  40912  hbtlem6  40954  mptrcllem  41221  rntrcl  41236  dfrcl2  41282  relexpss1d  41313  rfovcnvf1od  41612  supcnvlimsup  43281  fourierdlem42  43690  sge0less  43930
  Copyright terms: Public domain W3C validator