Theorem rnss 5950

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

Syntax hints:   → wi 4   ⊆ wss 3951  ^◡ccnv 5684  dom cdm 5685  ran crn 5686

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  rnssi  5951  imass1  6119  imass2  6120  ssxpb  6194  sofld  6207  resssxp  6290  funssxp  6764  dff2  7119  dff3  7120  fliftf  7335  1stcof  8044  2ndcof  8045  frxp  8151  frxp2  8169  frxp3  8176  fodomfi  9350  fodomfiOLD  9370  marypha1lem  9473  marypha1  9474  dfac12lem2  10185  fpwwe2lem12  10682  prdsvallem  17499  prdsval  17500  prdsbas  17502  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  prdshom  17512  catcfuccl  18163  catcxpccl  18252  odf1o2  19591  dprdres  20048  lmss  23306  txss12  23613  txbasval  23614  fmss  23954  tsmsxplem1  24161  ustimasn  24237  utopbas  24244  metustexhalf  24569  causs  25332  ovoliunlem1  25537  dvcnvrelem1  26056  taylf  26402  subgrprop3  29293  sspba  30746  imadifxp  32614  gsumpart  33060  metideq  33892  sxbrsigalem5  34290  omsmon  34300  carsggect  34320  carsgclctunlem2  34321  heicant  37662  mblfinlem1  37664  symrefref2  38564  dicval  41178  aks6d1c2  42131  rntrclfvOAI  42702  diophrw  42770  dnnumch2  43057  lmhmlnmsplit  43099  hbtlem6  43141  mptrcllem  43626  rntrcl  43641  dfrcl2  43687  relexpss1d  43718  rfovcnvf1od  44017  supcnvlimsup  45755  fourierdlem42  46164  sge0less  46407  isubgredgss  47851