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

Theorem sseq1d 3094
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 3088 . 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 1314    C_ wss 3039
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  sseq12d  3096  eqsstrd  3101  snssg  3624  ssiun2s  3825  treq  4000  onsucsssucexmid  4410  funimass1  5168  feq1  5223  sbcfg  5239  fvmptssdm  5471  fvimacnvi  5500  nnsucsssuc  6354  ereq1  6402  elpm2r  6526  fipwssg  6833  nnnninf  6989  ctssexmid  6990  iscnp  12274  iscnp4  12293  cnntr  12300  cnconst2  12308  cnptopresti  12313  cnptoprest  12314  txbas  12333  txcnp  12346  txdis  12352  txdis1cn  12353  blssps  12502  blss  12503  ssblex  12506  blin2  12507  metss2  12573  metrest  12581  metcnp3  12586  cnopnap  12669  limccl  12703  ellimc3apf  12704
  Copyright terms: Public domain W3C validator