Theorem rnss 5934

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908  ^◡ccnv 5665  dom cdm 5666  ran crn 5667

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-cnv 5674  df-dm 5676  df-rn 5677

This theorem is used by:  rnssi  5935  imass1  6108  imass2  6109  ssxpb  6177  sofld  6190  resssxp  6277  funssxp  6741  dff2  7101  dff3  7102  fliftf  7324  1stcof  8025  2ndcof  8026  frxp  8131  frxp2  8149  frxp3  8156  fodomfi  9282  marypha1lem  9403  marypha1  9404  dfac12lem2  10147  fpwwe2lem12  10645  prdsvallem  17532  prdsval  17533  prdsbas  17535  prdsplusg  17536  prdsmulr  17537  prdsvsca  17538  prdshom  17545  catcfuccl  18200  catcxpccl  18288  odf1o2  19674  dprdres  20131  lmss  23492  txss12  23799  txbasval  23800  fmss  24140  tsmsxplem1  24347  ustimasn  24422  utopbas  24429  metustexhalf  24750  causs  25494  ovoliunlem1  25698  dvcnvrelem1  26213  taylf  26561  subgrprop3  29663  sspba  31116  imadifxp  32983  gsumpart  33414  metideq  34314  sxbrsigalem5  34709  omsmon  34719  carsggect  34739  carsgclctunlem2  34740  heicant  38346  mblfinlem1  38348  symrefref2  39336  dicval  41990  aks6d1c2  42937  rntrclfvOAI  43462  diophrw  43530  dnnumch2  43812  lmhmlnmsplit  43854  hbtlem6  43896  mptrcllem  44379  rntrcl  44394  dfrcl2  44440  relexpss1d  44471  rfovcnvf1od  44770  supcnvlimsup  46494  fourierdlem42  46903  sge0less  47146  isubgredgss  48670