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

Theorem sseq2 3089
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 3072 . . . 4  |-  ( C 
C_  A  ->  ( A  C_  B  ->  C  C_  B ) )
21com12 30 . . 3  |-  ( A 
C_  B  ->  ( C  C_  A  ->  C  C_  B ) )
3 sstr2 3072 . . . 4  |-  ( C 
C_  B  ->  ( B  C_  A  ->  C  C_  A ) )
43com12 30 . . 3  |-  ( B 
C_  A  ->  ( C  C_  B  ->  C  C_  A ) )
52, 4anim12i 334 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  C_  A  ->  C  C_  B
)  /\  ( C  C_  B  ->  C  C_  A
) ) )
6 eqss 3080 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
7 dfbi2 383 . 2  |-  ( ( C  C_  A  <->  C  C_  B
)  <->  ( ( C 
C_  A  ->  C  C_  B )  /\  ( C  C_  B  ->  C  C_  A ) ) )
85, 6, 73imtr4i 200 1  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1314    C_ wss 3039
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  sseq12  3090  sseq2i  3092  sseq2d  3095  sseqtrid  3115  nssne1  3123  sseq0  3372  un00  3377  pweq  3481  ssintab  3756  ssintub  3757  intmin  3759  treq  4000  ssexg  4035  exmidundif  4097  frforeq3  4237  frirrg  4240  iunpw  4369  ordtri2orexmid  4406  ontr2exmid  4408  onsucsssucexmid  4410  ordtri2or2exmid  4454  fununi  5159  funcnvuni  5160  feq3  5225  ssimaexg  5449  nnawordex  6390  ereq1  6402  xpider  6466  domeng  6612  ssfiexmid  6736  fisseneq  6786  sbthlemi4  6814  sbthlemi5  6815  acfun  7027  ccfunen  7043  basis2  12110  eltg2  12117  clsval  12175  ntrcls0  12195  isnei  12208  neiint  12209  neipsm  12218  opnneissb  12219  opnssneib  12220  innei  12227  icnpimaex  12275  cnptoprest2  12304  neitx  12332  txcnp  12335  blssps  12491  blss  12492  metss  12558  metrest  12570  metcnp3  12575  bdssexg  12913  bj-nntrans  12960  bj-omtrans  12965
  Copyright terms: Public domain W3C validator