Theorem rnss 5889

Description: Subset theorem for range. (Contributed by NM, 22-Mar-1998.)

Assertion

Ref	Expression
rnss	⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)

Proof of Theorem rnss

Step	Hyp	Ref	Expression
1		cnvss 5822	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		dmss 5852	. . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵)
4		df-rn 5636	. 2 ⊢ ran 𝐴 = dom ◡𝐴
5		df-rn 5636	. 2 ⊢ ran 𝐵 = dom ◡𝐵
6	3, 4, 5	3sstr4g 3988	1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3902  ^◡ccnv 5624  dom cdm 5625  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  rnssi  5890  imass1  6061  imass2  6062  ssxpb  6133  sofld  6146  resssxp  6229  funssxp  6691  dff2  7046  dff3  7047  fliftf  7263  1stcof  7965  2ndcof  7966  frxp  8070  frxp2  8088  frxp3  8095  fodomfi  9216  fodomfiOLD  9234  marypha1lem  9340  marypha1  9341  dfac12lem2  10059  fpwwe2lem12  10557  prdsvallem  17378  prdsval  17379  prdsbas  17381  prdsplusg  17382  prdsmulr  17383  prdsvsca  17384  prdshom  17391  catcfuccl  18046  catcxpccl  18134  odf1o2  19506  dprdres  19963  lmss  23246  txss12  23553  txbasval  23554  fmss  23894  tsmsxplem1  24101  ustimasn  24176  utopbas  24183  metustexhalf  24504  causs  25258  ovoliunlem1  25463  dvcnvrelem1  25982  taylf  26328  subgrprop3  29332  sspba  30785  imadifxp  32658  gsumpart  33127  metideq  34031  sxbrsigalem5  34426  omsmon  34436  carsggect  34456  carsgclctunlem2  34457  heicant  37827  mblfinlem1  37829  symrefref2  38819  dicval  41473  aks6d1c2  42421  rntrclfvOAI  42969  diophrw  43037  dnnumch2  43323  lmhmlnmsplit  43365  hbtlem6  43407  mptrcllem  43890  rntrcl  43905  dfrcl2  43951  relexpss1d  43982  rfovcnvf1od  44281  supcnvlimsup  46020  fourierdlem42  46429  sge0less  46672  isubgredgss  48147