Theorem rnss 5876

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

Syntax hints:   → wi 4   ⊆ wss 3900  ^◡ccnv 5613  dom cdm 5614  ran crn 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-opab 5152  df-cnv 5622  df-dm 5624  df-rn 5625

This theorem is referenced by:  rnssi  5877  imass1  6047  imass2  6048  ssxpb  6118  sofld  6131  resssxp  6213  funssxp  6675  dff2  7027  dff3  7028  fliftf  7244  1stcof  7946  2ndcof  7947  frxp  8051  frxp2  8069  frxp3  8076  fodomfi  9191  fodomfiOLD  9209  marypha1lem  9312  marypha1  9313  dfac12lem2  10028  fpwwe2lem12  10525  prdsvallem  17350  prdsval  17351  prdsbas  17353  prdsplusg  17354  prdsmulr  17355  prdsvsca  17356  prdshom  17363  catcfuccl  18017  catcxpccl  18105  odf1o2  19478  dprdres  19935  lmss  23206  txss12  23513  txbasval  23514  fmss  23854  tsmsxplem1  24061  ustimasn  24136  utopbas  24143  metustexhalf  24464  causs  25218  ovoliunlem1  25423  dvcnvrelem1  25942  taylf  26288  subgrprop3  29247  sspba  30697  imadifxp  32571  gsumpart  33027  metideq  33896  sxbrsigalem5  34291  omsmon  34301  carsggect  34321  carsgclctunlem2  34322  heicant  37674  mblfinlem1  37676  symrefref2  38579  dicval  41194  aks6d1c2  42142  rntrclfvOAI  42703  diophrw  42771  dnnumch2  43057  lmhmlnmsplit  43099  hbtlem6  43141  mptrcllem  43625  rntrcl  43640  dfrcl2  43686  relexpss1d  43717  rfovcnvf1od  44016  supcnvlimsup  45757  fourierdlem42  46166  sge0less  46409  isubgredgss  47875