Theorem rnss 5847

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

Syntax hints:   → wi 4   ⊆ wss 3892  ^◡ccnv 5589  dom cdm 5590  ran crn 5591

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-cnv 5598  df-dm 5600  df-rn 5601

This theorem is referenced by:  rnssi  5848  imass1  6008  imass2  6009  ssxpb  6076  sofld  6089  resssxp  6172  funssxp  6627  dff2  6972  dff3  6973  fliftf  7182  1stcof  7854  2ndcof  7855  frxp  7958  fodomfi  9070  marypha1lem  9170  marypha1  9171  dfac12lem2  9901  fpwwe2lem12  10399  prdsvallem  17163  prdsval  17164  prdsbas  17166  prdsplusg  17167  prdsmulr  17168  prdsvsca  17169  prdshom  17176  catcfuccl  17832  catcfucclOLD  17833  catcxpccl  17922  catcxpcclOLD  17923  odf1o2  19176  dprdres  19629  lmss  22447  txss12  22754  txbasval  22755  fmss  23095  tsmsxplem1  23302  ustimasn  23378  utopbas  23385  metustexhalf  23710  causs  24460  ovoliunlem1  24664  dvcnvrelem1  25179  taylf  25518  subgrprop3  27641  sspba  29085  imadifxp  30936  gsumpart  31311  metideq  31839  sxbrsigalem5  32251  omsmon  32261  carsggect  32281  carsgclctunlem2  32282  frxp2  33787  frxp3  33793  heicant  35808  mblfinlem1  35810  symrefref2  36673  dicval  39186  rntrclfvOAI  40510  diophrw  40578  dnnumch2  40867  lmhmlnmsplit  40909  hbtlem6  40951  mptrcllem  41191  rntrcl  41206  dfrcl2  41252  relexpss1d  41283  rfovcnvf1od  41582  supcnvlimsup  43252  fourierdlem42  43661  sge0less  43901