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

Theorem sseq2 3179
Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
sseq2  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )

Proof of Theorem sseq2
StepHypRef Expression
1 sstr2 3162 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 30 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3162 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 30 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 338 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3170 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 388 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 201 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
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  sseq2i  3182  sseq2d  3185  sseqtrid  3205  nssne1  3213  sseq0  3464  un00  3469  pweq  3577  ssintab  3859  ssintub  3860  intmin  3862  treq  4104  ssexg  4139  exmidundif  4203  frforeq3  4344  frirrg  4347  iunpw  4477  ordtri2orexmid  4519  ontr2exmid  4521  onsucsssucexmid  4523  ordtri2or2exmid  4567  ontri2orexmidim  4568  fununi  5280  funcnvuni  5281  feq3  5346  ssimaexg  5574  nnawordex  6524  ereq1  6536  xpider  6600  domeng  6746  ssfiexmid  6870  fisseneq  6925  sbthlemi4  6953  sbthlemi5  6954  acfun  7200  onntri45  7234  ccfunen  7254  fprodssdc  11582  basis2  13213  eltg2  13220  clsval  13278  ntrcls0  13298  isnei  13311  neiint  13312  neipsm  13321  opnneissb  13322  opnssneib  13323  innei  13330  icnpimaex  13378  cnptoprest2  13407  neitx  13435  txcnp  13438  blssps  13594  blss  13595  metss  13661  metrest  13673  metcnp3  13678  bdssexg  14312  bj-nntrans  14359  bj-omtrans  14364
  Copyright terms: Public domain W3C validator