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

Theorem eqsstr3i 3209
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 2287 . 2  |-  A  =  B
3 eqsstr3.2 . 2  |-  B  C_  C
42, 3eqsstri 3208 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    C_ wss 3152
This theorem is referenced by:  inss2  3390  dmv  4894  ofrfval  6086  ofval  6087  ofrval  6088  off  6093  ofres  6094  ofco  6097  dftpos4  6253  smores2  6371  onwf  7502  r0weon  7640  cda1dif  7802  unctb  7831  infmap2  7844  itunitc  8047  axcclem  8083  dfnn3  9760  bcm1k  11327  bcpasc  11333  ressbasss  13200  strlemor1  13235  prdsle  13361  prdsless  13362  dprd2da  15277  opsrle  16217  indiscld  16828  leordtval2  16942  fiuncmp  17131  prdstopn  17322  itg1addlem4  19054  itg1addlem5  19055  tdeglem4  19446  aannenlem3  19710  efifo  19909  advlogexp  20002  pjoml4i  22166  5oai  22240  3oai  22247  bdopssadj  22661  ballotlemodife  23056  subfacp1lem5  23126  filnetlem3  25741  filnetlem4  25742  stoweidlem34  27195  relopabVD  28050  psubspset  29306  psubclsetN  29498
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator