Theorem rnssi 5846

Description: Subclass inference for range. (Contributed by Peter Mazsa, 24-Sep-2022.)

Hypothesis

Ref	Expression
rnssi.1	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
rnssi	⊢ ran 𝐴 ⊆ ran 𝐵

Proof of Theorem rnssi

Step	Hyp	Ref	Expression
1		rnssi.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		rnss 5845	. 2 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 ⊆ ran 𝐵

Syntax hints:   ⊆ wss 3891  ran crn 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-cnv 5596  df-dm 5598  df-rn 5599

This theorem is referenced by:  rnresss  5924  ssrnres  6078  fssres  6636  smores  8167  rnttrcl  9441  brdom4  10270  smobeth  10326  nqerf  10670  catcoppccl  17813  catcoppcclOLD  17814  lern  18290  gsumzres  19491  gsumzaddlem  19503  gsumzadd  19504  dprdfadd  19604  txkgen  22784  dvlog  25787  perpln2  27053  pfxrn2  31193  fixssrn  34188  cnvrcl0  41186