Theorem rnss 5886

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

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

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 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  rnssi  5887  imass1  6058  imass2  6059  ssxpb  6130  sofld  6143  resssxp  6226  funssxp  6688  dff2  7043  dff3  7044  fliftf  7261  1stcof  7963  2ndcof  7964  frxp  8067  frxp2  8085  frxp3  8092  fodomfi  9213  fodomfiOLD  9231  marypha1lem  9337  marypha1  9338  dfac12lem2  10056  fpwwe2lem12  10554  prdsvallem  17406  prdsval  17407  prdsbas  17409  prdsplusg  17410  prdsmulr  17411  prdsvsca  17412  prdshom  17419  catcfuccl  18074  catcxpccl  18162  odf1o2  19537  dprdres  19994  lmss  23272  txss12  23579  txbasval  23580  fmss  23920  tsmsxplem1  24127  ustimasn  24202  utopbas  24209  metustexhalf  24530  causs  25274  ovoliunlem1  25478  dvcnvrelem1  25994  taylf  26339  subgrprop3  29364  sspba  30818  imadifxp  32691  gsumpart  33144  metideq  34058  sxbrsigalem5  34453  omsmon  34463  carsggect  34483  carsgclctunlem2  34484  heicant  37987  mblfinlem1  37989  symrefref2  38979  dicval  41633  aks6d1c2  42580  rntrclfvOAI  43134  diophrw  43202  dnnumch2  43488  lmhmlnmsplit  43530  hbtlem6  43572  mptrcllem  44055  rntrcl  44070  dfrcl2  44116  relexpss1d  44147  rfovcnvf1od  44446  supcnvlimsup  46183  fourierdlem42  46592  sge0less  46835  isubgredgss  48338