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

Theorem eqsstr3i 3669
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 2660 . 2 𝐴 = 𝐵
3 eqsstr3.2 . 2 𝐵𝐶
42, 3eqsstri 3668 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  inss2  3867  dmv  5373  ofrfval  6947  ofval  6948  ofrval  6949  off  6954  ofres  6955  ofco  6959  dftpos4  7416  smores2  7496  onwf  8731  r0weon  8873  cda1dif  9036  unctb  9065  infmap2  9078  itunitc  9281  axcclem  9317  dfnn3  11072  cotr2  13762  ressbasss  15979  strlemor1OLD  16016  prdsle  16169  prdsless  16170  dprd2da  18487  opsrle  19523  indiscld  20943  leordtval2  21064  fiuncmp  21255  prdstopn  21479  ustneism  22074  itg1addlem4  23511  itg1addlem5  23512  tdeglem4  23865  aannenlem3  24130  efifo  24338  konigsbergssiedgw  27228  pjoml4i  28574  5oai  28648  3oai  28655  bdopssadj  29068  xrge00  29814  xrge0mulc1cn  30115  esumdivc  30273  rpsqrtcn  30799  subfacp1lem5  31292  filnetlem3  32500  filnetlem4  32501  mblfinlem4  33579  itg2gt0cn  33595  psubspset  35348  psubclsetN  35540  relexpaddss  38327  corcltrcl  38348  relopabVD  39451  cncfiooicc  40425  amgmwlem  42876
  Copyright terms: Public domain W3C validator