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

Theorem sseq2i 3587
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 3584 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wss 3534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-in 3541  df-ss 3548
This theorem is referenced by:  sseqtri  3594  syl6sseq  3608  abss  3628  ssrab  3637  ssindif0  3977  difcom  3999  ssunsn2  4291  ssunpr  4295  sspr  4296  sstp  4297  ssintrab  4424  iunpwss  4540  dffun2  5795  ssimaex  6153  elpwun  6841  frfi  8062  alephislim  8761  cardaleph  8767  fin1a2lem12  9088  zornn0g  9182  ssxr  9953  nnwo  11580  isstruct  15646  issubm  17111  grpissubg  17378  islinds  19904  basdif0  20505  tgdif0  20544  cmpsublem  20949  cmpsub  20950  hauscmplem  20956  2ndcctbss  21005  fbncp  21390  cnextfval  21613  eltsms  21683  reconn  22366  axcontlem3  25559  axcontlem4  25560  chsscon1i  27506  hatomistici  28406  chirredlem4  28437  atabs2i  28446  mdsymlem1  28447  mdsymlem3  28449  mdsymlem6  28452  mdsymlem8  28454  dmdbr5ati  28466  iundifdif  28564  nocvxminlem  30890  nocvxmin  30891  poimir  32410  ismblfin  32418  ntrk0kbimka  37155  ntrclsk3  37186  ntrneicls11  37206  abssf  38124  ssrabf  38127  stoweidlem57  38749  ovnsubadd  39261  ovnovollem3  39347  propssopi  40122  umgredg  40368  nbuhgr  40562  uhgrvd00  40747  issubmgm  41576  linccl  41994  lincdifsn  42004
  Copyright terms: Public domain W3C validator