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

Theorem sseq2i 3384
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 3381 . 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 1369    C_ wss 3331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3338  df-ss 3345
This theorem is referenced by:  sseqtri  3391  syl6sseq  3405  abss  3424  ssrab  3433  ssindif0  3735  difcom  3766  ssunsn2  4035  ssunpr  4038  sspr  4039  sstp  4040  ssintrab  4154  iunpwss  4263  dffun2  5431  ssimaex  5759  elpwun  6392  frfi  7560  alephislim  8256  cardaleph  8262  fin1a2lem12  8583  zornn0g  8677  ssxr  9447  nnwo  10923  isstruct  14187  issubm  15478  grpissubg  15704  islinds  18241  basdif0  18561  tgdif0  18600  cmpsublem  19005  cmpsub  19006  hauscmplem  19012  2ndcctbss  19062  fbncp  19415  cnextfval  19637  eltsms  19706  reconn  20408  axcontlem3  23215  axcontlem4  23216  chsscon1i  24868  hatomistici  25769  chirredlem4  25800  atabs2i  25809  mdsymlem1  25810  mdsymlem3  25812  mdsymlem6  25815  mdsymlem8  25817  dmdbr5ati  25829  iundifdif  25916  nocvxminlem  27834  nocvxmin  27835  ismblfin  28435  stoweidlem57  29855  linccl  30951  lincdifsn  30961
  Copyright terms: Public domain W3C validator