Theorem rnss 5888

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

Syntax hints:   → wi 4   ⊆ wss 3890  ^◡ccnv 5624  dom cdm 5625  ran crn 5626

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 2712

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 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  rnssi  5889  imass1  6060  imass2  6061  ssxpb  6132  sofld  6145  resssxp  6228  funssxp  6690  dff2  7047  dff3  7048  fliftf  7266  1stcof  7968  2ndcof  7969  frxp  8073  frxp2  8091  frxp3  8098  fodomfi  9219  fodomfiOLD  9237  marypha1lem  9343  marypha1  9344  dfac12lem2  10065  fpwwe2lem12  10563  prdsvallem  17415  prdsval  17416  prdsbas  17418  prdsplusg  17419  prdsmulr  17420  prdsvsca  17421  prdshom  17428  catcfuccl  18083  catcxpccl  18171  odf1o2  19546  dprdres  20003  lmss  23288  txss12  23595  txbasval  23596  fmss  23936  tsmsxplem1  24143  ustimasn  24218  utopbas  24225  metustexhalf  24546  causs  25290  ovoliunlem1  25494  dvcnvrelem1  26009  taylf  26351  subgrprop3  29370  sspba  30823  imadifxp  32697  gsumpart  33151  metideq  34084  sxbrsigalem5  34479  omsmon  34489  carsggect  34509  carsgclctunlem2  34510  heicant  38023  mblfinlem1  38025  symrefref2  39015  dicval  41669  aks6d1c2  42616  rntrclfvOAI  43141  diophrw  43209  dnnumch2  43491  lmhmlnmsplit  43533  hbtlem6  43575  mptrcllem  44058  rntrcl  44073  dfrcl2  44119  relexpss1d  44150  rfovcnvf1od  44449  supcnvlimsup  46184  fourierdlem42  46593  sge0less  46836  isubgredgss  48357