Theorem rnss 5921

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 5850	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		dmss 5884	. . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵)
3	1, 2	syl 18	. 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵)
4		df-rn 5662	. 2 ⊢ ran 𝐴 = dom ◡𝐴
5		df-rn 5662	. 2 ⊢ ran 𝐵 = dom ◡𝐵
6	3, 4, 5	3sstr4g 3984	1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ^◡ccnv 5650  dom cdm 5651  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  rnssi  5922  imass1  6095  imass2  6096  ssxpb  6165  sofld  6178  resssxp  6265  funssxp  6730  dff2  7091  dff3  7092  fliftf  7315  1stcof  8020  2ndcof  8021  frxp  8127  frxp2  8145  frxp3  8152  fodomfi  9288  marypha1lem  9409  marypha1  9410  dfac12lem2  10204  fpwwe2lem12  10708  prdsvallem  17605  prdsval  17606  prdsbas  17608  prdsplusg  17609  prdsmulr  17610  prdsvsca  17611  prdshom  17618  catcfuccl  18273  catcxpccl  18361  odf1o2  19767  dprdres  20224  lmss  23596  txss12  23904  txbasval  23905  fmss  24245  tsmsxplem1  24452  ustimasn  24527  utopbas  24534  metustexhalf  24855  causs  25599  ovoliunlem1  25803  dvcnvrelem1  26317  taylf  26670  subgrprop3  29839  sspba  31311  imadifxp  33177  gsumpart  33606  metideq  34507  sxbrsigalem5  34903  omsmon  34913  carsggect  34933  carsgclctunlem2  34934  heicant  38541  mblfinlem1  38543  symrefref2  39547  dicval  42201  aks6d1c2  43148  rntrclfvOAI  43655  diophrw  43723  dnnumch2  44005  lmhmlnmsplit  44047  hbtlem6  44089  mptrcllem  44572  rntrcl  44587  dfrcl2  44633  relexpss1d  44664  rfovcnvf1od  44963  supcnvlimsup  46694  fourierdlem42  47103  sge0less  47346  isubgredgss  48907