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

Theorem sseq2i 3529
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 3526 . 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 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  sseqtri  3536  syl6sseq  3550  abss  3569  ssrab  3578  ssindif0  3880  difcom  3911  ssunsn2  4186  ssunpr  4189  sspr  4190  sstp  4191  ssintrab  4305  iunpwss  4415  dffun2  5596  ssimaex  5930  elpwun  6591  frfi  7761  alephislim  8460  cardaleph  8466  fin1a2lem12  8787  zornn0g  8881  ssxr  9650  nnwo  11143  isstruct  14496  issubm  15788  grpissubg  16016  islinds  18611  basdif0  19221  tgdif0  19260  cmpsublem  19665  cmpsub  19666  hauscmplem  19672  2ndcctbss  19722  fbncp  20075  cnextfval  20297  eltsms  20366  reconn  21068  axcontlem3  23945  axcontlem4  23946  chsscon1i  26056  hatomistici  26957  chirredlem4  26988  atabs2i  26997  mdsymlem1  26998  mdsymlem3  27000  mdsymlem6  27003  mdsymlem8  27005  dmdbr5ati  27017  iundifdif  27103  nocvxminlem  29027  nocvxmin  29028  ismblfin  29632  stoweidlem57  31357  fourierdlem57  31464  linccl  32088  lincdifsn  32098
  Copyright terms: Public domain W3C validator