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

Theorem sseq2i 3432
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 3429 . 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 187    = wceq 1437    C_ wss 3379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3386  df-ss 3393
This theorem is referenced by:  sseqtri  3439  syl6sseq  3453  abss  3473  ssrab  3482  ssindif0  3791  difcom  3825  ssunsn2  4102  ssunpr  4105  sspr  4106  sstp  4107  ssintrab  4222  iunpwss  4335  dffun2  5554  ssimaex  5890  elpwun  6562  frfi  7769  alephislim  8465  cardaleph  8471  fin1a2lem12  8792  zornn0g  8886  ssxr  9654  nnwo  11175  isstruct  15074  issubm  16537  grpissubg  16780  islinds  19309  basdif0  19910  tgdif0  19950  cmpsublem  20356  cmpsub  20357  hauscmplem  20363  2ndcctbss  20412  fbncp  20796  cnextfval  21019  eltsms  21089  reconn  21788  axcontlem3  24938  axcontlem4  24939  chsscon1i  27057  hatomistici  27957  chirredlem4  27988  atabs2i  27997  mdsymlem1  27998  mdsymlem3  28000  mdsymlem6  28003  mdsymlem8  28005  dmdbr5ati  28017  iundifdif  28124  nocvxminlem  30528  nocvxmin  30529  poimir  31880  ismblfin  31888  stoweidlem57  37801  ovnsubadd  38241  propssopi  38809  umgredg  38991  nbuhgr  39147  issubmgm  39380  linccl  39800  lincdifsn  39810
  Copyright terms: Public domain W3C validator