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

Theorem eqsstr3i 3830
 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 2806 . 2 𝐴 = 𝐵
3 eqsstr3.2 . 2 𝐵𝐶
42, 3eqsstri 3829 1 𝐴𝐶
 Colors of variables: wff setvar class Syntax hints:   = wceq 1653   ⊆ wss 3767 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775 This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781 This theorem is referenced by:  inss2  4027  dmv  5542  idssxp  5671  ofrfval  7137  ofval  7138  ofrval  7139  off  7144  ofres  7145  ofco  7149  dftpos4  7607  smores2  7688  onwf  8941  r0weon  9119  cda1dif  9284  unctb  9313  infmap2  9326  itunitc  9529  axcclem  9565  dfnn3  11326  cotr2  14056  ressbasss  16254  prdsle  16434  prdsless  16435  dprd2da  18754  opsrle  19795  indiscld  21221  leordtval2  21342  fiuncmp  21533  prdstopn  21757  ustneism  22352  itg1addlem4  23804  itg1addlem5  23805  tdeglem4  24158  aannenlem3  24423  efifo  24632  konigsbergssiedgw  27589  pjoml4i  28963  5oai  29037  3oai  29044  bdopssadj  29457  xrge00  30194  xrge0mulc1cn  30495  esumdivc  30653  rpsqrtcn  31183  subfacp1lem5  31675  filnetlem3  32879  filnetlem4  32880  mblfinlem4  33930  itg2gt0cn  33945  psubspset  35757  psubclsetN  35949  relexpaddss  38781  corcltrcl  38802  relopabVD  39885  cncfiooicc  40839  amgmwlem  43338
 Copyright terms: Public domain W3C validator