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

Theorem sseq12d 3096
Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
Hypotheses
Ref Expression
sseq1d.1  |-  ( ph  ->  A  =  B )
sseq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
sseq12d  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  D ) )

Proof of Theorem sseq12d
StepHypRef Expression
1 sseq1d.1 . . 3  |-  ( ph  ->  A  =  B )
21sseq1d 3094 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
3 sseq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43sseq2d 3095 . 2  |-  ( ph  ->  ( B  C_  C  <->  B 
C_  D ) )
52, 4bitrd 187 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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:  3sstr3d  3109  3sstr4d  3110  ssdifeq0  3413  relcnvtr  5026  rdgisucinc  6248  oawordriexmid  6332  nnaword  6373  nnawordi  6377  sbthlem2  6812  isbth  6821  infnninf  6988  nnnninf  6989  ennnfonelemkh  11820  ennnfonelemrnh  11824  isstruct2im  11864  isstruct2r  11865  ressid2  11913  ressval2  11914  basis1  12109  baspartn  12112  eltg  12116  metss  12558  0nninf  12999  nninff  13000  nnsf  13001  peano4nninf  13002  nninfalllemn  13004  nninfalllem1  13005  nninfself  13011
  Copyright terms: Public domain W3C validator