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

Theorem eqsstr3i 3785
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 2780 . 2 𝐴 = 𝐵
3 eqsstr3.2 . 2 𝐵𝐶
42, 3eqsstri 3784 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737
This theorem is referenced by:  inss2  3982  dmv  5478  ofrfval  7056  ofval  7057  ofrval  7058  off  7063  ofres  7064  ofco  7068  dftpos4  7527  smores2  7608  onwf  8861  r0weon  9039  cda1dif  9204  unctb  9233  infmap2  9246  itunitc  9449  axcclem  9485  dfnn3  11240  cotr2  13926  ressbasss  16139  strlemor1OLD  16177  prdsle  16330  prdsless  16331  dprd2da  18649  opsrle  19690  indiscld  21116  leordtval2  21237  fiuncmp  21428  prdstopn  21652  ustneism  22247  itg1addlem4  23686  itg1addlem5  23687  tdeglem4  24040  aannenlem3  24305  efifo  24514  konigsbergssiedgw  27430  pjoml4i  28786  5oai  28860  3oai  28867  bdopssadj  29280  xrge00  30026  xrge0mulc1cn  30327  esumdivc  30485  rpsqrtcn  31011  subfacp1lem5  31504  filnetlem3  32712  filnetlem4  32713  mblfinlem4  33781  itg2gt0cn  33796  psubspset  35551  psubclsetN  35743  relexpaddss  38534  corcltrcl  38555  relopabVD  39657  cncfiooicc  40620  amgmwlem  43074
  Copyright terms: Public domain W3C validator