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

Theorem sseq1d 3176
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 3170 . 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 1348    C_ wss 3121
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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134
This theorem is referenced by:  sseq12d  3178  eqsstrd  3183  snssg  3716  ssiun2s  3917  treq  4093  onsucsssucexmid  4511  funimass1  5275  feq1  5330  sbcfg  5346  fvmptssdm  5580  fvimacnvi  5610  nnsucsssuc  6471  ereq1  6520  elpm2r  6644  fipwssg  6956  nnnninf  7102  ctssexmid  7126  iscnp  12993  iscnp4  13012  cnntr  13019  cnconst2  13027  cnptopresti  13032  cnptoprest  13033  txbas  13052  txcnp  13065  txdis  13071  txdis1cn  13072  blssps  13221  blss  13222  ssblex  13225  blin2  13226  metss2  13292  metrest  13300  metcnp3  13305  cnopnap  13388  limccl  13422  ellimc3apf  13423
  Copyright terms: Public domain W3C validator