Theorem rnss 5928

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  ^◡ccnv 5654  dom cdm 5655  ran crn 5656

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  rnssi  5929  imass1  6066  imass2  6067  ssxpb  6178  sofld  6191  resssxp  6290  funssxp  6760  dff2  7123  dff3  7124  fliftf  7346  1stcof  8055  2ndcof  8056  frxp  8165  frxp2  8188  frxp3  8195  fodomfi  9332  marypha1lem  9452  marypha1  9453  dfac12lem2  10250  fpwwe2lem12  10754  prdsvallem  17654  prdsval  17655  prdsbas  17657  prdsplusg  17658  prdsmulr  17659  prdsvsca  17660  prdshom  17667  catcfuccl  18322  catcxpccl  18410  odf1o2  19817  dprdres  20274  lmss  23646  txss12  23954  txbasval  23955  fmss  24295  tsmsxplem1  24502  ustimasn  24577  utopbas  24584  metustexhalf  24905  causs  25649  ovoliunlem1  25853  dvcnvrelem1  26367  taylf  26718  subgrprop3  29887  sspba  31359  imadifxp  33267  gsumpart  33694  metideq  34595  sxbrsigalem5  34990  omsmon  35000  carsggect  35020  carsgclctunlem2  35021  heicant  38765  mblfinlem1  38767  symrefref2  39771  dicval  42425  aks6d1c2  43372  rntrclfvOAI  43895  diophrw  43963  dnnumch2  44245  lmhmlnmsplit  44282  hbtlem6  44323  mptrcllem  44805  rntrcl  44820  dfrcl2  44866  relexpss1d  44897  rfovcnvf1od  45196  rnhfstructsshf  46225  supcnvlimsup  46955  fourierdlem42  47364  sge0less  47607  isubgredgss  49168