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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  rnssi  5887  imass1  6057  imass2  6058  ssxpb  6129  sofld  6142  resssxp  6225  funssxp  6687  dff2  7041  dff3  7042  fliftf  7258  1stcof  7960  2ndcof  7961  frxp  8065  frxp2  8083  frxp3  8090  fodomfi  9206  fodomfiOLD  9224  marypha1lem  9327  marypha1  9328  dfac12lem2  10046  fpwwe2lem12  10543  prdsvallem  17368  prdsval  17369  prdsbas  17371  prdsplusg  17372  prdsmulr  17373  prdsvsca  17374  prdshom  17381  catcfuccl  18035  catcxpccl  18123  odf1o2  19495  dprdres  19952  lmss  23223  txss12  23530  txbasval  23531  fmss  23871  tsmsxplem1  24078  ustimasn  24153  utopbas  24160  metustexhalf  24481  causs  25235  ovoliunlem1  25440  dvcnvrelem1  25959  taylf  26305  subgrprop3  29265  sspba  30718  imadifxp  32592  gsumpart  33048  metideq  33917  sxbrsigalem5  34312  omsmon  34322  carsggect  34342  carsgclctunlem2  34343  heicant  37705  mblfinlem1  37707  symrefref2  38669  dicval  41285  aks6d1c2  42233  rntrclfvOAI  42798  diophrw  42866  dnnumch2  43152  lmhmlnmsplit  43194  hbtlem6  43236  mptrcllem  43720  rntrcl  43735  dfrcl2  43781  relexpss1d  43812  rfovcnvf1od  44111  supcnvlimsup  45852  fourierdlem42  46261  sge0less  46504  isubgredgss  47979