Theorem rnss 5931

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

Syntax hints:   → wi 4   ⊆ wss 3906  ^◡ccnv 5662  dom cdm 5663  ran crn 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is referenced by:  rnssi  5932  imass1  6105  imass2  6106  ssxpb  6174  sofld  6187  resssxp  6273  funssxp  6736  dff2  7096  dff3  7097  fliftf  7315  1stcof  8017  2ndcof  8018  frxp  8123  frxp2  8141  frxp3  8148  fodomfi  9273  marypha1lem  9394  marypha1  9395  dfac12lem2  10129  fpwwe2lem12  10628  prdsvallem  17508  prdsval  17509  prdsbas  17511  prdsplusg  17512  prdsmulr  17513  prdsvsca  17514  prdshom  17521  catcfuccl  18176  catcxpccl  18264  odf1o2  19644  dprdres  20101  lmss  23436  txss12  23743  txbasval  23744  fmss  24084  tsmsxplem1  24291  ustimasn  24366  utopbas  24373  metustexhalf  24694  causs  25438  ovoliunlem1  25642  dvcnvrelem1  26157  taylf  26502  subgrprop3  29604  sspba  31057  imadifxp  32924  gsumpart  33361  metideq  34261  sxbrsigalem5  34656  omsmon  34666  carsggect  34686  carsgclctunlem2  34687  heicant  38284  mblfinlem1  38286  symrefref2  39274  dicval  41928  aks6d1c2  42875  rntrclfvOAI  43402  diophrw  43470  dnnumch2  43752  lmhmlnmsplit  43794  hbtlem6  43836  mptrcllem  44319  rntrcl  44334  dfrcl2  44380  relexpss1d  44411  rfovcnvf1od  44710  supcnvlimsup  46434  fourierdlem42  46843  sge0less  47086  isubgredgss  48607