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

Theorem sseq12d 3186
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 3184 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
3 sseq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43sseq2d 3185 . 2  |-  ( ph  ->  ( B  C_  C  <->  B 
C_  D ) )
52, 4bitrd 188 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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:  3sstr3d  3199  3sstr4d  3200  ssdifeq0  3505  relcnvtr  5144  rdgisucinc  6380  oawordriexmid  6465  nnaword  6506  nnawordi  6510  sbthlem2  6951  isbth  6960  nninff  7115  infnninf  7116  infnninfOLD  7117  nnnninf  7118  nnnninfeq  7120  nnnninfeq2  7121  nninfwlpoimlemg  7167  ennnfonelemkh  12396  ennnfonelemrnh  12400  isstruct2im  12455  isstruct2r  12456  basis1  13212  baspartn  13215  eltg  13219  metss  13661  0nninf  14409  nnsf  14410  peano4nninf  14411  nninfalllem1  14413  nninfself  14418
  Copyright terms: Public domain W3C validator