MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnssi Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 rnssi.1 . 2 𝐴𝐵
2 rnss 5657 . 2 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
31, 2ax-mp 5 1 ran 𝐴 ⊆ ran 𝐵
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator