ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sseq1d Unicode version

Theorem sseq1d 3157
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
sseq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sseq1d  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )

Proof of Theorem sseq1d
StepHypRef Expression
1 sseq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sseq1 3151 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2syl 14 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1335    C_ wss 3102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115
This theorem is referenced by:  sseq12d  3159  eqsstrd  3164  snssg  3692  ssiun2s  3893  treq  4068  onsucsssucexmid  4486  funimass1  5247  feq1  5302  sbcfg  5318  fvmptssdm  5552  fvimacnvi  5581  nnsucsssuc  6439  ereq1  6487  elpm2r  6611  fipwssg  6923  nnnninf  7069  ctssexmid  7093  iscnp  12599  iscnp4  12618  cnntr  12625  cnconst2  12633  cnptopresti  12638  cnptoprest  12639  txbas  12658  txcnp  12671  txdis  12677  txdis1cn  12678  blssps  12827  blss  12828  ssblex  12831  blin2  12832  metss2  12898  metrest  12906  metcnp3  12911  cnopnap  12994  limccl  13028  ellimc3apf  13029
  Copyright terms: Public domain W3C validator