Theorem rnss 5952

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

Syntax hints:   → wi 4   ⊆ wss 3962  ^◡ccnv 5687  dom cdm 5688  ran crn 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699

This theorem is referenced by:  rnssi  5953  imass1  6121  imass2  6122  ssxpb  6195  sofld  6208  resssxp  6291  funssxp  6764  dff2  7118  dff3  7119  fliftf  7334  1stcof  8042  2ndcof  8043  frxp  8149  frxp2  8167  frxp3  8174  fodomfi  9347  fodomfiOLD  9367  marypha1lem  9470  marypha1  9471  dfac12lem2  10182  fpwwe2lem12  10679  prdsvallem  17500  prdsval  17501  prdsbas  17503  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  odf1o2  19605  dprdres  20062  lmss  23321  txss12  23628  txbasval  23629  fmss  23969  tsmsxplem1  24176  ustimasn  24252  utopbas  24259  metustexhalf  24584  causs  25345  ovoliunlem1  25550  dvcnvrelem1  26070  taylf  26416  subgrprop3  29307  sspba  30755  imadifxp  32620  gsumpart  33042  metideq  33853  sxbrsigalem5  34269  omsmon  34279  carsggect  34299  carsgclctunlem2  34300  heicant  37641  mblfinlem1  37643  symrefref2  38544  dicval  41158  aks6d1c2  42111  rntrclfvOAI  42678  diophrw  42746  dnnumch2  43033  lmhmlnmsplit  43075  hbtlem6  43117  mptrcllem  43602  rntrcl  43617  dfrcl2  43663  relexpss1d  43694  rfovcnvf1od  43993  supcnvlimsup  45695  fourierdlem42  46104  sge0less  46347  isubgredgss  47788