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

Theorem sseq1d 3184
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 3178 . 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 105    = wceq 1353    C_ wss 3129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142
This theorem is referenced by:  sseq12d  3186  eqsstrd  3191  snssgOLD  3728  ssiun2s  3930  treq  4107  onsucsssucexmid  4526  funimass1  5293  feq1  5348  sbcfg  5364  fvmptssdm  5600  fvimacnvi  5630  nnsucsssuc  6492  ereq1  6541  elpm2r  6665  fipwssg  6977  nnnninf  7123  ctssexmid  7147  iscnp  13669  iscnp4  13688  cnntr  13695  cnconst2  13703  cnptopresti  13708  cnptoprest  13709  txbas  13728  txcnp  13741  txdis  13747  txdis1cn  13748  blssps  13897  blss  13898  ssblex  13901  blin2  13902  metss2  13968  metrest  13976  metcnp3  13981  cnopnap  14064  limccl  14098  ellimc3apf  14099
  Copyright terms: Public domain W3C validator