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

Theorem sseq2i 3373
Description: An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
sseq1i.1  |-  A  =  B
Assertion
Ref Expression
sseq2i  |-  ( C 
C_  A  <->  C  C_  B
)

Proof of Theorem sseq2i
StepHypRef Expression
1 sseq1i.1 . 2  |-  A  =  B
2 sseq2 3370 . 2  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
31, 2ax-mp 8 1  |-  ( C 
C_  A  <->  C  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652    C_ wss 3320
This theorem is referenced by:  sseqtri  3380  syl6sseq  3394  abss  3412  ssrab  3421  ssindif0  3681  difcom  3712  ssunsn2  3958  ssunpr  3961  sspr  3962  sstp  3963  ssintrab  4073  iunpwss  4180  elpwun  4756  dffun2  5464  ssimaex  5788  frfi  7352  alephislim  7964  cardaleph  7970  fin1a2lem12  8291  zornn0g  8385  ssxr  9145  nnwo  10542  isstruct  13479  issubm  14748  basdif0  17018  tgdif0  17057  cmpsublem  17462  cmpsub  17463  hauscmplem  17469  2ndcctbss  17518  fbncp  17871  cnextfval  18093  eltsms  18162  reconn  18859  chsscon1i  22964  hatomistici  23865  chirredlem4  23896  atabs2i  23905  mdsymlem1  23906  mdsymlem3  23908  mdsymlem6  23911  mdsymlem8  23913  dmdbr5ati  23925  iundifdif  24013  nocvxminlem  25645  nocvxmin  25646  axcontlem3  25905  axcontlem4  25906  ismblfin  26247  islinds  27256  stoweidlem57  27782  swrd0  28183
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator