Theorem rnss 5896

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

Syntax hints:   → wi 4   ⊆ wss 3903  ^◡ccnv 5631  dom cdm 5632  ran crn 5633

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  rnssi  5897  imass1  6068  imass2  6069  ssxpb  6140  sofld  6153  resssxp  6236  funssxp  6698  dff2  7053  dff3  7054  fliftf  7271  1stcof  7973  2ndcof  7974  frxp  8078  frxp2  8096  frxp3  8103  fodomfi  9224  fodomfiOLD  9242  marypha1lem  9348  marypha1  9349  dfac12lem2  10067  fpwwe2lem12  10565  prdsvallem  17386  prdsval  17387  prdsbas  17389  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdshom  17399  catcfuccl  18054  catcxpccl  18142  odf1o2  19514  dprdres  19971  lmss  23254  txss12  23561  txbasval  23562  fmss  23902  tsmsxplem1  24109  ustimasn  24184  utopbas  24191  metustexhalf  24512  causs  25266  ovoliunlem1  25471  dvcnvrelem1  25990  taylf  26336  subgrprop3  29361  sspba  30814  imadifxp  32687  gsumpart  33156  metideq  34070  sxbrsigalem5  34465  omsmon  34475  carsggect  34495  carsgclctunlem2  34496  heicant  37895  mblfinlem1  37897  symrefref2  38887  dicval  41541  aks6d1c2  42489  rntrclfvOAI  43037  diophrw  43105  dnnumch2  43391  lmhmlnmsplit  43433  hbtlem6  43475  mptrcllem  43958  rntrcl  43973  dfrcl2  44019  relexpss1d  44050  rfovcnvf1od  44349  supcnvlimsup  46087  fourierdlem42  46496  sge0less  46739  isubgredgss  48214