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

Theorem sseq2i 3369
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 3366 . 2  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
31, 2ax-mp 5 1  |-  ( C 
C_  A  <->  C  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  sseqtri  3376  syl6sseq  3390  abss  3409  ssrab  3418  ssindif0  3720  difcom  3751  ssunsn2  4020  ssunpr  4023  sspr  4024  sstp  4025  ssintrab  4139  iunpwss  4248  dffun2  5416  ssimaex  5744  elpwun  6378  frfi  7545  alephislim  8241  cardaleph  8247  fin1a2lem12  8568  zornn0g  8662  ssxr  9432  nnwo  10908  isstruct  14167  issubm  15457  grpissubg  15681  islinds  18080  basdif0  18400  tgdif0  18439  cmpsublem  18844  cmpsub  18845  hauscmplem  18851  2ndcctbss  18901  fbncp  19254  cnextfval  19476  eltsms  19545  reconn  20247  axcontlem3  23035  axcontlem4  23036  chsscon1i  24688  hatomistici  25589  chirredlem4  25620  atabs2i  25629  mdsymlem1  25630  mdsymlem3  25632  mdsymlem6  25635  mdsymlem8  25637  dmdbr5ati  25649  iundifdif  25737  nocvxminlem  27678  nocvxmin  27679  ismblfin  28276  stoweidlem57  29698  linccl  30678  lincdifsn  30688
  Copyright terms: Public domain W3C validator