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

Theorem eqsstr3i 3463
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 2460 . 2  |-  A  =  B
3 eqsstr3.2 . 2  |-  B  C_  C
42, 3eqsstri 3462 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1444    C_ wss 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418
This theorem is referenced by:  inss2  3653  dmv  5050  ofrfval  6539  ofval  6540  ofrval  6541  off  6546  ofres  6547  ofco  6551  dftpos4  6992  smores2  7073  onwf  8301  r0weon  8443  cda1dif  8606  unctb  8635  infmap2  8648  itunitc  8851  axcclem  8887  dfnn3  10623  bcm1k  12500  bcpasc  12506  cotr2  13041  ressbasss  15181  strlemor1  15217  prdsle  15360  prdsless  15361  dprd2da  17675  opsrle  18699  indiscld  20107  leordtval2  20228  fiuncmp  20419  prdstopn  20643  ustneism  21238  itg1addlem4  22657  itg1addlem5  22658  tdeglem4  23009  aannenlem3  23286  efifo  23496  advlogexp  23600  pjoml4i  27240  5oai  27314  3oai  27321  bdopssadj  27734  suppss2fOLD  28237  xrge00  28448  xrge0mulc1cn  28747  esumdivc  28904  ballotlemodife  29330  subfacp1lem5  29907  filnetlem3  31036  filnetlem4  31037  mblfinlem4  31980  itg2gt0cn  31997  psubspset  33309  psubclsetN  33501  relexpaddss  36310  corcltrcl  36331  relopabVD  37298  cncfiooicc  37772  stoweidlem34  37895
  Copyright terms: Public domain W3C validator