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

Theorem eqsstr3i 3534
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)
Hypotheses
Ref Expression
eqsstr3.1
eqsstr3.2
Assertion
Ref Expression
eqsstr3i

Proof of Theorem eqsstr3i
StepHypRef Expression
1 eqsstr3.1 . . 3
21eqcomi 2470 . 2
3 eqsstr3.2 . 2
42, 3eqsstri 3533 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  C_wss 3475
This theorem is referenced by:  inss2  3718  dmv  5223  ofrfval  6548  ofval  6549  ofrval  6550  off  6554  ofres  6555  ofco  6560  dftpos4  6993  smores2  7044  onwf  8269  r0weon  8411  cda1dif  8577  unctb  8606  infmap2  8619  itunitc  8822  axcclem  8858  dfnn3  10575  bcm1k  12393  bcpasc  12399  ressbasss  14689  strlemor1  14724  prdsle  14859  prdsless  14860  dprd2da  17091  opsrle  18140  indiscld  19592  leordtval2  19713  fiuncmp  19904  prdstopn  20129  ustneism  20726  itg1addlem4  22106  itg1addlem5  22107  tdeglem4  22458  aannenlem3  22726  efifo  22934  advlogexp  23036  pjoml4i  26505  5oai  26579  3oai  26586  bdopssadj  27000  suppss2f  27477  xrge00  27674  xrge0mulc1cn  27923  esumdivc  28089  ballotlemodife  28436  subfacp1lem5  28628  mblfinlem4  30054  itg2gt0cn  30070  filnetlem3  30198  filnetlem4  30199  cncfiooicc  31697  stoweidlem34  31816  relopabVD  33701  psubspset  35468  psubclsetN  35660  cotr2  37787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator