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

Theorem eqsstrri 3927
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)
Hypotheses
Ref Expression
eqsstr3.1 𝐵 = 𝐴
eqsstr3.2 𝐵𝐶
Assertion
Ref Expression
eqsstrri 𝐴𝐶

Proof of Theorem eqsstrri
StepHypRef Expression
1 eqsstr3.1 . . 3 𝐵 = 𝐴
21eqcomi 2767 . 2 𝐴 = 𝐵
3 eqsstr3.2 . 2 𝐵𝐶
42, 3eqsstri 3926 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wss 3858
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 2113  ax-9 2121  ax-ext 2729
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875
This theorem is referenced by:  inss2  4134  dmv  5763  idssxp  5888  ofrfvalg  7412  ofval  7415  ofrval  7416  off  7422  ofres  7423  ofco  7427  dftpos4  7921  smores2  8001  onwf  9292  r0weon  9472  dju1dif  9632  unctb  9665  infmap2  9678  itunitc  9881  axcclem  9917  dfnn3  11688  cotr2  14384  ressbasss  16614  prdsle  16793  prdsless  16794  cntrss  18527  dprd2da  19232  opsrle  20807  indiscld  21791  leordtval2  21912  fiuncmp  22104  prdstopn  22328  ustneism  22924  itg1addlem4  24399  itg1addlem5  24400  tdeglem4OLD  24760  aannenlem3  25025  efifo  25238  konigsbergssiedgw  28134  pjoml4i  29469  5oai  29543  3oai  29550  bdopssadj  29963  xrge00  30821  xrge0mulc1cn  31412  esumdivc  31570  rpsqrtcn  32092  subfacp1lem5  32662  filnetlem3  34118  filnetlem4  34119  mblfinlem4  35377  itg2gt0cn  35392  psubspset  37320  psubclsetN  37512  dvrelog2  39630  dvrelog3  39631  relexpaddss  40792  corcltrcl  40813  relopabVD  41980  cncfiooicc  42902  amgmwlem  45721
  Copyright terms: Public domain W3C validator