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

Theorem sseq1 3178
Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sseq1  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )

Proof of Theorem sseq1
StepHypRef Expression
1 eqss 3170 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
2 sstr2 3162 . . . 4  |-  ( B 
C_  A  ->  ( A  C_  C  ->  B  C_  C ) )
32adantl 277 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  ->  B  C_  C )
)
4 sstr2 3162 . . . 4  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
54adantr 276 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( B  C_  C  ->  A  C_  C )
)
63, 5impbid 129 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  <->  B 
C_  C ) )
71, 6sylbi 121 1  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> 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:  sseq12  3180  sseq1i  3181  sseq1d  3184  nssne2  3214  sbss  3531  pwjust  3575  elpw  3580  elpwg  3582  sssnr  3751  ssprr  3754  sstpr  3755  unimax  3841  trss  4107  elssabg  4145  bnd2  4170  exmidexmid  4193  exmidsssn  4199  exmidsssnc  4200  mss  4222  exss  4223  frforeq2  4341  ordtri2orexmid  4518  ontr2exmid  4520  onsucsssucexmid  4522  reg2exmidlema  4529  sucprcreg  4544  ordtri2or2exmid  4566  ontri2orexmidim  4567  onintexmid  4568  tfis  4578  tfisi  4582  elomssom  4600  nnregexmid  4616  releq  4704  xpsspw  4734  iss  4948  relcnvtr  5143  iotass  5190  fununi  5279  funcnvuni  5280  funimaexglem  5294  ffoss  5488  ssimaex  5572  tfrlem1  6302  el2oss1o  6437  nnsucsssuc  6486  qsss  6587  phpm  6858  ssfiexmid  6869  findcard2d  6884  findcard2sd  6885  diffifi  6887  isinfinf  6890  fiintim  6921  fisseneq  6924  fidcenumlemrk  6946  fidcenumlemr  6947  sbthlem2  6950  isbth  6959  ctssdclemr  7104  onntri45  7233  elinp  7451  sup3exmid  8890  zfz1isolem1  10791  zfz1iso  10792  fimaxre2  11206  sumeq1  11334  fsum2d  11414  fsumabs  11444  fsumiun  11456  prodeq1f  11531  fprod2d  11602  exmidunben  12397  ctiunct  12411  ssomct  12416  restsspw  12633  uniopn  13132  fiinopn  13135  fiinbas  13180  baspartn  13181  eltg2  13186  eltg3  13190  topbas  13200  clsval  13244  neival  13276  neiint  13278  neipsm  13287  opnneissb  13288  opnssneib  13289  innei  13296  restbasg  13301  cnpdis  13375  txbas  13391  eltx  13392  neitx  13401  txlm  13412  blssexps  13562  blssex  13563  neibl  13624  metrest  13639  xmettx  13643  tgioo  13679  tgqioo  13680  limcimolemlt  13766  recnprss  13789  bj-om  14311  bj-2inf  14312  bj-nntrans  14325  bj-omtrans  14330  exmid1stab  14372  subctctexmid  14373  pw1nct  14375
  Copyright terms: Public domain W3C validator