Theorem rnssi 5658

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 5657	. 2 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 ⊆ ran 𝐵

Syntax hints:   ⊆ wss 3831  ran crn 5412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-rab 3099  df-v 3419  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-sn 4445  df-pr 4447  df-op 4451  df-br 4935  df-opab 4997  df-cnv 5419  df-dm 5421  df-rn 5422

This theorem is referenced by:  ssrnres  5880  fssres  6378  smores  7799  brdom4  9756  smobeth  9812  nqerf  10156  catcoppccl  17238  lern  17705  gsumzres  18795  gsumzaddlem  18806  gsumzadd  18807  dprdfadd  18904  txkgen  21979  dvlog  24950  perpln2  26214  fixssrn  32929  rnresss  40900