Theorem rnss 5920

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895  ^◡ccnv 5649  dom cdm 5650  ran crn 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  rnssi  5921  imass1  6053  imass2  6054  ssxpb  6165  sofld  6178  resssxp  6272  funssxp  6738  dff2  7099  dff3  7100  fliftf  7323  1stcof  8031  2ndcof  8032  frxp  8140  frxp2  8163  frxp3  8170  fodomfi  9307  marypha1lem  9428  marypha1  9429  dfac12lem2  10226  fpwwe2lem12  10730  prdsvallem  17630  prdsval  17631  prdsbas  17633  prdsplusg  17634  prdsmulr  17635  prdsvsca  17636  prdshom  17643  catcfuccl  18298  catcxpccl  18386  odf1o2  19792  dprdres  20249  lmss  23621  txss12  23929  txbasval  23930  fmss  24270  tsmsxplem1  24477  ustimasn  24552  utopbas  24559  metustexhalf  24880  causs  25624  ovoliunlem1  25828  dvcnvrelem1  26342  taylf  26693  subgrprop3  29862  sspba  31334  imadifxp  33242  gsumpart  33670  metideq  34571  sxbrsigalem5  34966  omsmon  34976  carsggect  34996  carsgclctunlem2  34997  heicant  38666  mblfinlem1  38668  symrefref2  39672  dicval  42326  aks6d1c2  43273  rntrclfvOAI  43795  diophrw  43863  dnnumch2  44145  lmhmlnmsplit  44182  hbtlem6  44224  mptrcllem  44706  rntrcl  44721  dfrcl2  44767  relexpss1d  44798  rfovcnvf1od  45097  rnhfstructsshf  46120  supcnvlimsup  46843  fourierdlem42  47252  sge0less  47495  isubgredgss  49056