Theorem rnss 5964

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

Syntax hints:   → wi 4   ⊆ wss 3976  ^◡ccnv 5699  dom cdm 5700  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  rnssi  5965  imass1  6131  imass2  6132  ssxpb  6205  sofld  6218  resssxp  6301  funssxp  6776  dff2  7133  dff3  7134  fliftf  7351  1stcof  8060  2ndcof  8061  frxp  8167  frxp2  8185  frxp3  8192  fodomfi  9378  fodomfiOLD  9398  marypha1lem  9502  marypha1  9503  dfac12lem2  10214  fpwwe2lem12  10711  prdsvallem  17514  prdsval  17515  prdsbas  17517  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  prdshom  17527  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  odf1o2  19615  dprdres  20072  lmss  23327  txss12  23634  txbasval  23635  fmss  23975  tsmsxplem1  24182  ustimasn  24258  utopbas  24265  metustexhalf  24590  causs  25351  ovoliunlem1  25556  dvcnvrelem1  26076  taylf  26420  subgrprop3  29311  sspba  30759  imadifxp  32623  gsumpart  33038  metideq  33839  sxbrsigalem5  34253  omsmon  34263  carsggect  34283  carsgclctunlem2  34284  heicant  37615  mblfinlem1  37617  symrefref2  38519  dicval  41133  aks6d1c2  42087  rntrclfvOAI  42647  diophrw  42715  dnnumch2  43002  lmhmlnmsplit  43044  hbtlem6  43086  mptrcllem  43575  rntrcl  43590  dfrcl2  43636  relexpss1d  43667  rfovcnvf1od  43966  supcnvlimsup  45661  fourierdlem42  46070  sge0less  46313