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

Theorem eqsstr3i 3371
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 2439 . 2  |-  A  =  B
3 eqsstr3.2 . 2  |-  B  C_  C
42, 3eqsstri 3370 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    C_ wss 3312
This theorem is referenced by:  inss2  3554  dmv  5077  ofrfval  6305  ofval  6306  ofrval  6307  off  6312  ofres  6313  ofco  6316  dftpos4  6490  smores2  6608  onwf  7748  r0weon  7886  cda1dif  8048  unctb  8077  infmap2  8090  itunitc  8293  axcclem  8329  dfnn3  10006  bcm1k  11598  bcpasc  11604  ressbasss  13513  strlemor1  13548  prdsle  13676  prdsless  13677  dprd2da  15592  opsrle  16528  indiscld  17147  leordtval2  17268  fiuncmp  17459  prdstopn  17652  ustneism  18245  itg1addlem4  19583  itg1addlem5  19584  tdeglem4  19975  aannenlem3  20239  efifo  20441  advlogexp  20538  pjoml4i  23081  5oai  23155  3oai  23162  bdopssadj  23576  suppss2f  24041  xrge00  24200  xrge0mulc1cn  24319  esumdivc  24465  ballotlemodife  24747  subfacp1lem5  24862  mblfinlem3  26236  itg2gt0cn  26250  filnetlem3  26400  filnetlem4  26401  stoweidlem34  27750  relopabVD  28950  psubspset  30478  psubclsetN  30670
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator