Theorem rnss 5386

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

Syntax hints:   → wi 4   ⊆ wss 3607  ^◡ccnv 5142  dom cdm 5143  ran crn 5144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-cnv 5151  df-dm 5153  df-rn 5154

This theorem is referenced by:  imass1  5535  imass2  5536  ssxpb  5603  ssrnres  5607  sofld  5616  funssxp  6099  fssres  6108  dff2  6411  dff3  6412  fliftf  6605  1stcof  7240  2ndcof  7241  frxp  7332  smores  7494  fodomfi  8280  marypha1lem  8380  marypha1  8381  dfac12lem2  9004  brdom4  9390  smobeth  9446  fpwwe2lem13  9502  nqerf  9790  prdsval  16162  prdsbas  16164  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  prdshom  16174  catcoppccl  16805  catcfuccl  16806  catcxpccl  16894  lern  17272  odf1o2  18034  gsumzres  18356  gsumzaddlem  18367  gsumzadd  18368  dprdfadd  18465  dprdres  18473  lmss  21150  txss12  21456  txbasval  21457  txkgen  21503  fmss  21797  tsmsxplem1  22003  ustimasn  22079  utopbas  22086  metustexhalf  22408  causs  23142  ovoliunlem1  23316  dvcnvrelem1  23825  taylf  24160  dvlog  24442  perpln2  25651  subgrprop3  26213  sspba  27710  imadifxp  29540  metideq  30064  sxbrsigalem5  30478  omsmon  30488  carsggect  30508  carsgclctunlem2  30509  fixssrn  32139  heicant  33574  mblfinlem1  33576  symrefref2  34447  dicval  36782  rntrclfvOAI  37571  diophrw  37639  dnnumch2  37932  lmhmlnmsplit  37974  hbtlem6  38016  mptrcllem  38237  cnvrcl0  38249  rntrcl  38252  dfrcl2  38283  relexpss1d  38314  rp-imass  38382  rfovcnvf1od  38615  rnresss  39679  supcnvlimsup  40290  fourierdlem42  40684  sge0less  40927