Theorem rnss 5691

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

Syntax hints:   → wi 4   ⊆ wss 3859  ^◡ccnv 5442  dom cdm 5443  ran crn 5444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-br 4963  df-opab 5025  df-cnv 5451  df-dm 5453  df-rn 5454

This theorem is referenced by:  rnssi  5692  imass1  5840  imass2  5841  ssxpb  5907  sofld  5920  funssxp  6403  dff2  6728  dff3  6729  fliftf  6931  1stcof  7575  2ndcof  7576  frxp  7673  fodomfi  8643  marypha1lem  8743  marypha1  8744  dfac12lem2  9416  fpwwe2lem13  9910  prdsval  16557  prdsbas  16559  prdsplusg  16560  prdsmulr  16561  prdsvsca  16562  prdshom  16569  catcfuccl  17198  catcxpccl  17286  odf1o2  18428  dprdres  18867  lmss  21590  txss12  21897  txbasval  21898  fmss  22238  tsmsxplem1  22444  ustimasn  22520  utopbas  22527  metustexhalf  22849  causs  23584  ovoliunlem1  23786  dvcnvrelem1  24297  taylf  24632  subgrprop3  26741  sspba  28195  imadifxp  30041  metideq  30750  sxbrsigalem5  31163  omsmon  31173  carsggect  31193  carsgclctunlem2  31194  heicant  34477  mblfinlem1  34479  symrefref2  35349  dicval  37862  rntrclfvOAI  38792  diophrw  38860  dnnumch2  39149  lmhmlnmsplit  39191  hbtlem6  39233  mptrcllem  39477  rntrcl  39492  dfrcl2  39523  relexpss1d  39554  rp-imass  39621  rfovcnvf1od  39854  supcnvlimsup  41582  fourierdlem42  41996  sge0less  42236