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

Theorem sseq2i 3203
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 3200 . 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 176    = wceq 1623    C_ wss 3152
This theorem is referenced by:  sseqtri  3210  syl6sseq  3224  abss  3242  ssrab  3251  ssindif0  3508  difcom  3538  ssunsn2  3773  ssunpr  3776  sspr  3777  sstp  3778  ssintrab  3885  iunpwss  3991  elpwun  4567  dffun2  5265  ssimaex  5584  frfi  7102  alephislim  7710  cardaleph  7716  fin1a2lem12  8037  zornn0g  8132  ssxr  8892  nnwo  10284  isstruct  13158  issubm  14425  basdif0  16691  tgdif0  16730  cmpsublem  17126  cmpsub  17127  hauscmplem  17133  2ndcctbss  17181  fbncp  17534  eltsms  17815  reconn  18333  chsscon1i  22041  hatomistici  22942  chirredlem4  22973  atabs2i  22982  mdsymlem1  22983  mdsymlem3  22985  mdsymlem6  22988  mdsymlem8  22990  dmdbr5ati  23002  rinvf1o  23038  nocvxminlem  24344  nocvxmin  24345  axcontlem3  24594  axcontlem4  24595  idsubc  25851  islinds  27279  stoweidlem53  27802  stoweidlem57  27806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator