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

Theorem sseq2i 3237
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 3234 . 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 1633    C_ wss 3186
This theorem is referenced by:  sseqtri  3244  syl6sseq  3258  abss  3276  ssrab  3285  ssindif0  3542  difcom  3572  ssunsn2  3810  ssunpr  3813  sspr  3814  sstp  3815  ssintrab  3922  iunpwss  4028  elpwun  4604  dffun2  5302  ssimaex  5622  frfi  7147  alephislim  7755  cardaleph  7761  fin1a2lem12  8082  zornn0g  8177  ssxr  8937  nnwo  10331  isstruct  13205  issubm  14474  basdif0  16747  tgdif0  16786  cmpsublem  17182  cmpsub  17183  hauscmplem  17189  2ndcctbss  17237  fbncp  17586  eltsms  17867  reconn  18385  chsscon1i  22096  hatomistici  22997  chirredlem4  23028  atabs2i  23037  mdsymlem1  23038  mdsymlem3  23040  mdsymlem6  23043  mdsymlem8  23045  dmdbr5ati  23057  rinvf1o  23192  cnextfval  23412  nocvxminlem  24729  nocvxmin  24730  axcontlem3  24980  axcontlem4  24981  islinds  26427  stoweidlem53  26950  stoweidlem57  26954
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-in 3193  df-ss 3200
  Copyright terms: Public domain W3C validator