Theorem rnss 5885

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 5819	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		dmss 5849	. . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵)
4		df-rn 5634	. 2 ⊢ ran 𝐴 = dom ◡𝐴
5		df-rn 5634	. 2 ⊢ ran 𝐵 = dom ◡𝐵
6	3, 4, 5	3sstr4g 3991	1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3905  ^◡ccnv 5622  dom cdm 5623  ran crn 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-cnv 5631  df-dm 5633  df-rn 5634

This theorem is referenced by:  rnssi  5886  imass1  6056  imass2  6057  ssxpb  6127  sofld  6140  resssxp  6222  funssxp  6684  dff2  7037  dff3  7038  fliftf  7256  1stcof  7961  2ndcof  7962  frxp  8066  frxp2  8084  frxp3  8091  fodomfi  9219  fodomfiOLD  9239  marypha1lem  9342  marypha1  9343  dfac12lem2  10058  fpwwe2lem12  10555  prdsvallem  17376  prdsval  17377  prdsbas  17379  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  prdshom  17389  catcfuccl  18043  catcxpccl  18131  odf1o2  19470  dprdres  19927  lmss  23201  txss12  23508  txbasval  23509  fmss  23849  tsmsxplem1  24056  ustimasn  24132  utopbas  24139  metustexhalf  24460  causs  25214  ovoliunlem1  25419  dvcnvrelem1  25938  taylf  26284  subgrprop3  29239  sspba  30689  imadifxp  32563  gsumpart  33023  metideq  33859  sxbrsigalem5  34255  omsmon  34265  carsggect  34285  carsgclctunlem2  34286  heicant  37634  mblfinlem1  37636  symrefref2  38539  dicval  41155  aks6d1c2  42103  rntrclfvOAI  42664  diophrw  42732  dnnumch2  43018  lmhmlnmsplit  43060  hbtlem6  43102  mptrcllem  43586  rntrcl  43601  dfrcl2  43647  relexpss1d  43678  rfovcnvf1od  43977  supcnvlimsup  45722  fourierdlem42  46131  sge0less  46374  isubgredgss  47849