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

Theorem sseq2i 3978
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 3975 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  sseqtri  3985  sseqtrdi  3999  abss  4022  ssrab  4035  ssindif0  4428  difcom  4451  ssunsn2  4792  ssunpr  4797  sspr  4798  sstp  4799  ssintrab  4937  iunpwss  5072  propssopi  5470  dffun2OLDOLD  6513  ssimaex  6931  elpwun  7708  ssfi  9124  frfi  9239  alephislim  10026  cardaleph  10032  fin1a2lem12  10354  zornn0g  10448  ssxr  11231  nnwo  12845  isstruct  17031  issubm  18621  grpissubg  18955  islinds  21231  basdif0  22319  tgdif0  22358  cmpsublem  22766  cmpsub  22767  hauscmplem  22773  2ndcctbss  22822  fbncp  23206  cnextfval  23429  eltsms  23500  reconn  24207  cmssmscld  24730  nocvxminlem  27139  nocvxmin  27140  axcontlem3  27957  axcontlem4  27958  umgredg  28131  nbuhgr  28333  uhgrvd00  28524  vtxdginducedm1  28533  chsscon1i  30446  hatomistici  31346  chirredlem4  31377  atabs2i  31386  mdsymlem1  31387  mdsymlem3  31389  mdsymlem6  31392  mdsymlem8  31394  dmdbr5ati  31406  iundifdif  31523  poimir  36140  ismblfin  36148  cossssid2  36959  ntrk0kbimka  42385  ntrclsk3  42416  ntrneicls11  42436  abssf  43396  ssrabf  43398  stoweidlem57  44372  ovnsubadd  44887  ovnovollem3  44973  issubmgm  46157  linccl  46569  lincdifsn  46579
  Copyright terms: Public domain W3C validator