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

Theorem eqsstr3i 3222
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 2300 . 2  |-  A  =  B
3 eqsstr3.2 . 2  |-  B  C_  C
42, 3eqsstri 3221 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632    C_ wss 3165
This theorem is referenced by:  inss2  3403  dmv  4910  ofrfval  6102  ofval  6103  ofrval  6104  off  6109  ofres  6110  ofco  6113  dftpos4  6269  smores2  6387  onwf  7518  r0weon  7656  cda1dif  7818  unctb  7847  infmap2  7860  itunitc  8063  axcclem  8099  dfnn3  9776  bcm1k  11343  bcpasc  11349  ressbasss  13216  strlemor1  13251  prdsle  13377  prdsless  13378  dprd2da  15293  opsrle  16233  indiscld  16844  leordtval2  16958  fiuncmp  17147  prdstopn  17338  itg1addlem4  19070  itg1addlem5  19071  tdeglem4  19462  aannenlem3  19726  efifo  19925  advlogexp  20018  pjoml4i  22182  5oai  22256  3oai  22263  bdopssadj  22677  ballotlemodife  23072  suppss2f  23216  xrge0mulc1cn  23338  esumdivc  23466  subfacp1lem5  23730  itg2gt0cn  25006  filnetlem3  26432  filnetlem4  26433  stoweidlem34  27886  relopabVD  28993  psubspset  30555  psubclsetN  30747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator