Theorem rnss 5919

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

Syntax hints:   → wi 4   ⊆ wss 3926  ^◡ccnv 5653  dom cdm 5654  ran crn 5655

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-cnv 5662  df-dm 5664  df-rn 5665

This theorem is referenced by:  rnssi  5920  imass1  6088  imass2  6089  ssxpb  6163  sofld  6176  resssxp  6259  funssxp  6733  dff2  7088  dff3  7089  fliftf  7307  1stcof  8016  2ndcof  8017  frxp  8123  frxp2  8141  frxp3  8148  fodomfi  9320  fodomfiOLD  9340  marypha1lem  9443  marypha1  9444  dfac12lem2  10157  fpwwe2lem12  10654  prdsvallem  17466  prdsval  17467  prdsbas  17469  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdshom  17479  catcfuccl  18129  catcxpccl  18217  odf1o2  19552  dprdres  20009  lmss  23234  txss12  23541  txbasval  23542  fmss  23882  tsmsxplem1  24089  ustimasn  24165  utopbas  24172  metustexhalf  24493  causs  25248  ovoliunlem1  25453  dvcnvrelem1  25972  taylf  26318  subgrprop3  29201  sspba  30654  imadifxp  32528  gsumpart  32997  metideq  33870  sxbrsigalem5  34266  omsmon  34276  carsggect  34296  carsgclctunlem2  34297  heicant  37625  mblfinlem1  37627  symrefref2  38527  dicval  41141  aks6d1c2  42089  rntrclfvOAI  42661  diophrw  42729  dnnumch2  43016  lmhmlnmsplit  43058  hbtlem6  43100  mptrcllem  43584  rntrcl  43599  dfrcl2  43645  relexpss1d  43676  rfovcnvf1od  43975  supcnvlimsup  45717  fourierdlem42  46126  sge0less  46369  isubgredgss  47826