MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqsstr3i Unicode version

Theorem eqsstr3i 3323
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)
Hypotheses
Ref Expression
eqsstr3.1  |-  B  =  A
eqsstr3.2  |-  B  C_  C
Assertion
Ref Expression
eqsstr3i  |-  A  C_  C

Proof of Theorem eqsstr3i
StepHypRef Expression
1 eqsstr3.1 . . 3  |-  B  =  A
21eqcomi 2392 . 2  |-  A  =  B
3 eqsstr3.2 . 2  |-  B  C_  C
42, 3eqsstri 3322 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649    C_ wss 3264
This theorem is referenced by:  inss2  3506  dmv  5026  ofrfval  6253  ofval  6254  ofrval  6255  off  6260  ofres  6261  ofco  6264  dftpos4  6435  smores2  6553  onwf  7690  r0weon  7828  cda1dif  7990  unctb  8019  infmap2  8032  itunitc  8235  axcclem  8271  dfnn3  9947  bcm1k  11534  bcpasc  11540  ressbasss  13449  strlemor1  13484  prdsle  13612  prdsless  13613  dprd2da  15528  opsrle  16464  indiscld  17079  leordtval2  17199  fiuncmp  17390  prdstopn  17582  ustneism  18175  itg1addlem4  19459  itg1addlem5  19460  tdeglem4  19851  aannenlem3  20115  efifo  20317  advlogexp  20414  pjoml4i  22938  5oai  23012  3oai  23019  bdopssadj  23433  suppss2f  23893  xrge00  24038  xrge0mulc1cn  24132  esumdivc  24270  ballotlemodife  24535  subfacp1lem5  24650  itg2gt0cn  25961  filnetlem3  26101  filnetlem4  26102  stoweidlem34  27452  relopabVD  28355  psubspset  29859  psubclsetN  30051
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-in 3271  df-ss 3278
  Copyright terms: Public domain W3C validator