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

Theorem rnssi 5778
 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 5777 . 2 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
31, 2ax-mp 5 1 ran 𝐴 ⊆ ran 𝐵
 Colors of variables: wff setvar class Syntax hints:   ⊆ wss 3884  ran crn 5524 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-cnv 5531  df-dm 5533  df-rn 5534 This theorem is referenced by:  rnresss  5858  ssrnres  6006  fssres  6522  smores  7976  brdom4  9945  smobeth  10001  nqerf  10345  catcoppccl  17363  lern  17830  gsumzres  19025  gsumzaddlem  19037  gsumzadd  19038  dprdfadd  19138  txkgen  22260  dvlog  25245  perpln2  26508  pfxrn2  30645  fixssrn  33476  cnvrcl0  40312
 Copyright terms: Public domain W3C validator