Theorem rnss 5895

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

Syntax hints:   → wi 4   ⊆ wss 3890  ^◡ccnv 5630  dom cdm 5631  ran crn 5632

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  rnssi  5896  imass1  6067  imass2  6068  ssxpb  6139  sofld  6152  resssxp  6235  funssxp  6697  dff2  7052  dff3  7053  fliftf  7270  1stcof  7972  2ndcof  7973  frxp  8076  frxp2  8094  frxp3  8101  fodomfi  9222  fodomfiOLD  9240  marypha1lem  9346  marypha1  9347  dfac12lem2  10067  fpwwe2lem12  10565  prdsvallem  17417  prdsval  17418  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  catcfuccl  18085  catcxpccl  18173  odf1o2  19548  dprdres  20005  lmss  23263  txss12  23570  txbasval  23571  fmss  23911  tsmsxplem1  24118  ustimasn  24193  utopbas  24200  metustexhalf  24521  causs  25265  ovoliunlem1  25469  dvcnvrelem1  25984  taylf  26326  subgrprop3  29345  sspba  30798  imadifxp  32671  gsumpart  33124  metideq  34037  sxbrsigalem5  34432  omsmon  34442  carsggect  34462  carsgclctunlem2  34463  heicant  37976  mblfinlem1  37978  symrefref2  38968  dicval  41622  aks6d1c2  42569  rntrclfvOAI  43123  diophrw  43191  dnnumch2  43473  lmhmlnmsplit  43515  hbtlem6  43557  mptrcllem  44040  rntrcl  44055  dfrcl2  44101  relexpss1d  44132  rfovcnvf1od  44431  supcnvlimsup  46168  fourierdlem42  46577  sge0less  46820  isubgredgss  48335