Theorem rnss 5882

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

Syntax hints:   → wi 4   ⊆ wss 3883  ^◡ccnv 5618  dom cdm 5619  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-br 5074  df-opab 5136  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  rnssi  5883  imass1  6054  imass2  6055  ssxpb  6126  sofld  6139  resssxp  6222  funssxp  6684  dff2  7041  dff3  7042  fliftf  7260  1stcof  7962  2ndcof  7963  frxp  8067  frxp2  8085  frxp3  8092  fodomfi  9213  fodomfiOLD  9231  marypha1lem  9337  marypha1  9338  dfac12lem2  10059  fpwwe2lem12  10557  prdsvallem  17409  prdsval  17410  prdsbas  17412  prdsplusg  17413  prdsmulr  17414  prdsvsca  17415  prdshom  17422  catcfuccl  18077  catcxpccl  18165  odf1o2  19540  dprdres  19997  lmss  23282  txss12  23589  txbasval  23590  fmss  23930  tsmsxplem1  24137  ustimasn  24212  utopbas  24219  metustexhalf  24540  causs  25284  ovoliunlem1  25488  dvcnvrelem1  26003  taylf  26345  subgrprop3  29364  sspba  30817  imadifxp  32691  gsumpart  33145  metideq  34086  sxbrsigalem5  34481  omsmon  34491  carsggect  34511  carsgclctunlem2  34512  heicant  38031  mblfinlem1  38033  symrefref2  39023  dicval  41677  aks6d1c2  42624  rntrclfvOAI  43149  diophrw  43217  dnnumch2  43499  lmhmlnmsplit  43541  hbtlem6  43583  mptrcllem  44066  rntrcl  44081  dfrcl2  44127  relexpss1d  44158  rfovcnvf1od  44457  supcnvlimsup  46191  fourierdlem42  46600  sge0less  46843  isubgredgss  48364