Theorem rnss 5906

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

Syntax hints:   → wi 4   ⊆ wss 3917  ^◡ccnv 5640  dom cdm 5641  ran crn 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-cnv 5649  df-dm 5651  df-rn 5652

This theorem is referenced by:  rnssi  5907  imass1  6075  imass2  6076  ssxpb  6150  sofld  6163  resssxp  6246  funssxp  6719  dff2  7074  dff3  7075  fliftf  7293  1stcof  8001  2ndcof  8002  frxp  8108  frxp2  8126  frxp3  8133  fodomfi  9268  fodomfiOLD  9288  marypha1lem  9391  marypha1  9392  dfac12lem2  10105  fpwwe2lem12  10602  prdsvallem  17424  prdsval  17425  prdsbas  17427  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdshom  17437  catcfuccl  18087  catcxpccl  18175  odf1o2  19510  dprdres  19967  lmss  23192  txss12  23499  txbasval  23500  fmss  23840  tsmsxplem1  24047  ustimasn  24123  utopbas  24130  metustexhalf  24451  causs  25205  ovoliunlem1  25410  dvcnvrelem1  25929  taylf  26275  subgrprop3  29210  sspba  30663  imadifxp  32537  gsumpart  33004  metideq  33890  sxbrsigalem5  34286  omsmon  34296  carsggect  34316  carsgclctunlem2  34317  heicant  37656  mblfinlem1  37658  symrefref2  38561  dicval  41177  aks6d1c2  42125  rntrclfvOAI  42686  diophrw  42754  dnnumch2  43041  lmhmlnmsplit  43083  hbtlem6  43125  mptrcllem  43609  rntrcl  43624  dfrcl2  43670  relexpss1d  43701  rfovcnvf1od  44000  supcnvlimsup  45745  fourierdlem42  46154  sge0less  46397  isubgredgss  47869