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

Theorem rnssi 5950
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 5949 . 2 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
31, 2ax-mp 5 1 ran 𝐴 ⊆ ran 𝐵
Colors of variables: wff setvar class
Syntax hints:  wss 3950  ran crn 5685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-cnv 5692  df-dm 5694  df-rn 5695
This theorem is referenced by:  rnresss  6034  ssrnres  6197  fssres  6773  smores  8393  rnttrcl  9763  brdom4  10571  smobeth  10627  nqerf  10971  catcoppccl  18163  lern  18637  gsumzres  19928  gsumzaddlem  19940  gsumzadd  19941  dprdfadd  20041  txkgen  23661  dvlog  26694  perpln2  28720  pfxrn2  32925  fixssrn  35909  cnvrcl0  43643
  Copyright terms: Public domain W3C validator