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

Theorem sseq1 3021
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 3015 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
2 sstr2 3007 . . . 4  |-  ( B 
C_  A  ->  ( A  C_  C  ->  B  C_  C ) )
32adantl 271 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  ->  B  C_  C )
)
4 sstr2 3007 . . . 4  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
54adantr 270 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( B  C_  C  ->  A  C_  C )
)
63, 5impbid 127 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  <->  B 
C_  C ) )
71, 6sylbi 119 1  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1285    C_ wss 2974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987
This theorem is referenced by:  sseq12  3023  sseq1i  3024  sseq1d  3027  nssne2  3057  sbss  3357  pwjust  3391  elpw  3396  elpwg  3398  sssnr  3553  ssprr  3556  sstpr  3557  unimax  3643  trss  3892  elssabg  3931  bnd2  3955  mss  3989  exss  3990  frforeq2  4108  ordtri2orexmid  4274  ontr2exmid  4276  onsucsssucexmid  4278  reg2exmidlema  4285  sucprcreg  4300  ordtri2or2exmid  4322  onintexmid  4323  tfis  4332  tfisi  4336  elnn  4354  nnregexmid  4368  releq  4448  xpsspw  4478  iss  4684  relcnvtr  4870  iotass  4914  fununi  4998  funcnvuni  4999  funimaexglem  5013  ffoss  5189  ssimaex  5266  tfrlem1  5957  nnsucsssuc  6136  qsss  6231  phpm  6400  ssfiexmid  6411  findcard2d  6425  findcard2sd  6426  diffifi  6428  elinp  6726  fimaxre2  10247  sumeq1  10330  bj-om  10890  bj-2inf  10891  bj-nntrans  10904  bj-omtrans  10909
  Copyright terms: Public domain W3C validator