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

Theorem sseq2i 3826
Description: An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
sseq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
sseq2i (𝐶𝐴𝐶𝐵)

Proof of Theorem sseq2i
StepHypRef Expression
1 sseq1i.1 . 2 𝐴 = 𝐵
2 sseq2 3823 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 198   = wceq 1653  wss 3769
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 2777
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 2786  df-cleq 2792  df-clel 2795  df-in 3776  df-ss 3783
This theorem is referenced by:  sseqtri  3833  syl6sseq  3847  abss  3867  ssrab  3876  ssindif0  4226  difcom  4247  ssunsn2  4546  ssunpr  4551  sspr  4552  sstp  4553  ssintrab  4690  iunpwss  4809  propssopi  5164  dffun2  6111  ssimaex  6488  elpwun  7211  frfi  8447  alephislim  9192  cardaleph  9198  fin1a2lem12  9521  zornn0g  9615  ssxr  10397  nnwo  11998  isstruct  16197  issubm  17662  grpissubg  17927  islinds  20473  basdif0  21086  tgdif0  21125  cmpsublem  21531  cmpsub  21532  hauscmplem  21538  2ndcctbss  21587  fbncp  21971  cnextfval  22194  eltsms  22264  reconn  22959  cmssmscld  23476  axcontlem3  26203  axcontlem4  26204  umgredg  26374  nbuhgr  26581  uhgrvd00  26784  vtxdginducedm1  26793  chsscon1i  28846  hatomistici  29746  chirredlem4  29777  atabs2i  29786  mdsymlem1  29787  mdsymlem3  29789  mdsymlem6  29792  mdsymlem8  29794  dmdbr5ati  29806  iundifdif  29898  nocvxminlem  32406  nocvxmin  32407  poimir  33931  ismblfin  33939  cossssid2  34712  ntrk0kbimka  39119  ntrclsk3  39150  ntrneicls11  39170  abssf  40053  ssrabf  40056  stoweidlem57  41017  ovnsubadd  41532  ovnovollem3  41618  issubmgm  42588  linccl  43002  lincdifsn  43012
  Copyright terms: Public domain W3C validator