Theorem rnss 5809

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

Syntax hints:   → wi 4   ⊆ wss 3936  ^◡ccnv 5554  dom cdm 5555  ran crn 5556

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  rnssi  5810  imass1  5964  imass2  5965  ssxpb  6031  sofld  6044  funssxp  6535  dff2  6865  dff3  6866  fliftf  7068  1stcof  7719  2ndcof  7720  frxp  7820  fodomfi  8797  marypha1lem  8897  marypha1  8898  dfac12lem2  9570  fpwwe2lem13  10064  prdsval  16728  prdsbas  16730  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  prdshom  16740  catcfuccl  17369  catcxpccl  17457  odf1o2  18698  dprdres  19150  lmss  21906  txss12  22213  txbasval  22214  fmss  22554  tsmsxplem1  22761  ustimasn  22837  utopbas  22844  metustexhalf  23166  causs  23901  ovoliunlem1  24103  dvcnvrelem1  24614  taylf  24949  subgrprop3  27058  sspba  28504  imadifxp  30351  metideq  31133  sxbrsigalem5  31546  omsmon  31556  carsggect  31576  carsgclctunlem2  31577  heicant  34942  mblfinlem1  34944  symrefref2  35814  dicval  38327  rntrclfvOAI  39337  diophrw  39405  dnnumch2  39694  lmhmlnmsplit  39736  hbtlem6  39778  mptrcllem  40022  rntrcl  40037  dfrcl2  40068  relexpss1d  40099  rp-imass  40166  rfovcnvf1od  40399  supcnvlimsup  42070  fourierdlem42  42483  sge0less  42723