Theorem rnss 5812

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

Syntax hints:   → wi 4   ⊆ wss 3939  ^◡ccnv 5557  dom cdm 5558  ran crn 5559

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5070  df-opab 5132  df-cnv 5566  df-dm 5568  df-rn 5569

This theorem is referenced by:  rnssi  5813  imass1  5967  imass2  5968  ssxpb  6034  sofld  6047  funssxp  6538  dff2  6868  dff3  6869  fliftf  7071  1stcof  7722  2ndcof  7723  frxp  7823  fodomfi  8800  marypha1lem  8900  marypha1  8901  dfac12lem2  9573  fpwwe2lem13  10067  prdsval  16731  prdsbas  16733  prdsplusg  16734  prdsmulr  16735  prdsvsca  16736  prdshom  16743  catcfuccl  17372  catcxpccl  17460  odf1o2  18701  dprdres  19153  lmss  21909  txss12  22216  txbasval  22217  fmss  22557  tsmsxplem1  22764  ustimasn  22840  utopbas  22847  metustexhalf  23169  causs  23904  ovoliunlem1  24106  dvcnvrelem1  24617  taylf  24952  subgrprop3  27061  sspba  28507  imadifxp  30354  metideq  31137  sxbrsigalem5  31550  omsmon  31560  carsggect  31580  carsgclctunlem2  31581  heicant  34931  mblfinlem1  34933  symrefref2  35803  dicval  38316  rntrclfvOAI  39294  diophrw  39362  dnnumch2  39651  lmhmlnmsplit  39693  hbtlem6  39735  mptrcllem  39979  rntrcl  39994  dfrcl2  40025  relexpss1d  40056  rp-imass  40123  rfovcnvf1od  40356  supcnvlimsup  42027  fourierdlem42  42441  sge0less  42681