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

Theorem sseq2i 3468
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 3465 . 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 189    = wceq 1454    C_ wss 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429
This theorem is referenced by:  sseqtri  3475  syl6sseq  3489  abss  3509  ssrab  3518  ssindif0  3829  difcom  3863  ssunsn2  4143  ssunpr  4146  sspr  4147  sstp  4148  ssintrab  4271  iunpwss  4384  dffun2  5610  ssimaex  5952  elpwun  6630  frfi  7841  alephislim  8539  cardaleph  8545  fin1a2lem12  8866  zornn0g  8960  ssxr  9728  nnwo  11252  isstruct  15179  issubm  16642  grpissubg  16885  islinds  19415  basdif0  20016  tgdif0  20056  cmpsublem  20462  cmpsub  20463  hauscmplem  20469  2ndcctbss  20518  fbncp  20902  cnextfval  21125  eltsms  21195  reconn  21894  axcontlem3  25044  axcontlem4  25045  chsscon1i  27163  hatomistici  28063  chirredlem4  28094  atabs2i  28103  mdsymlem1  28104  mdsymlem3  28106  mdsymlem6  28109  mdsymlem8  28111  dmdbr5ati  28123  iundifdif  28226  nocvxminlem  30627  nocvxmin  30628  poimir  32017  ismblfin  32025  stoweidlem57  37955  ovnsubadd  38431  propssopi  39039  umgredg  39276  nbuhgr  39460  uhgrvd00  39620  issubmgm  40061  linccl  40479  lincdifsn  40489
  Copyright terms: Public domain W3C validator