MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseq12d Structured version   Unicode version

Theorem sseq12d 3377
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 3375 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
3 sseq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43sseq2d 3376 . 2  |-  ( ph  ->  ( B  C_  C  <->  B 
C_  D ) )
52, 4bitrd 245 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    C_ wss 3320
This theorem is referenced by:  3sstr3d  3390  3sstr4d  3391  ssdifeq0  3710  relcnvtr  5389  knatar  6080  smogt  6629  oawordri  6793  omwordi  6814  omwordri  6815  oewordi  6834  oewordri  6835  oeworde  6836  nnawordi  6864  nnmwordi  6878  nnmwordri  6879  sbthlem2  7218  sbth  7227  marypha2lem3  7442  hartogslem1  7511  inf3lem1  7583  tcrank  7808  alephle  7969  cfsmolem  8150  isfin3ds  8209  fin23lem17  8218  fin23lem39  8230  isf32lem1  8233  isf32lem2  8234  isf32lem11  8243  isf33lem  8246  isf34lem7  8259  isf34lem6  8260  fin1a2lem13  8292  itunitc1  8300  dominf  8325  dcomex  8327  axdc2lem  8328  dominfac  8448  fpwwe2cbv  8505  fpwwe2lem2  8507  fpwwecbv  8519  fpwwelem  8520  canthwelem  8525  canthwe  8526  wunex2  8613  swrdval  11764  vdwpc  13348  vdwlem1  13349  vdwlem6  13354  vdwlem7  13355  vdwlem8  13356  isstruct2  13478  ressval  13516  mreexexlemd  13869  isacs1i  13882  isssc  14020  ssc2  14022  fullfunc  14103  fthfunc  14104  isps  14634  istsr  14649  isdir  14677  gsumvalx  14774  efgi2  15357  dmdprd  15559  dprdss  15587  dmdprdpr  15607  basis1  17015  baspartn  17019  eltg  17022  cncls  17338  ispnrm  17403  1stcfb  17508  2ndcctbss  17518  1stcelcls  17524  subislly  17544  kgenidm  17579  ptpjpre1  17603  txcmplem2  17674  flimval  17995  flimcf  18014  fclscf  18057  metss  18538  isngp  18643  iscph  19133  equivcau  19253  caubl  19260  caublcls  19261  ovoliunlem3  19400  volsuplem  19449  volsup  19450  dyaddisj  19488  itg1climres  19606  isausgra  21379  cusgrafilem1  21488  issh  22710  isch  22725  hsupss  22843  shslej  22882  shlub  22916  ledi  23042  pjoi0  23219  mdbr4  23801  dmdbr4  23809  dmdi4  23810  dmdbr5  23811  mdslle1i  23820  mdslle2i  23821  mdslmd1lem1  23828  mdslmd1lem2  23829  mdslmd1lem3  23830  mdslmd1lem4  23831  mdslmd1i  23832  sumdmdlem2  23922  zhmnrg  24351  cvmliftlem3  24974  dfrtrcl2  25148  volsupnfl  26251  ismrcd1  26752  ismrcd2  26753  ismrc  26755  incssnn0  26765  diophrw  26817  hbtlem5  27309  hbt  27311  lssatle  29813  pmaple  30558  2polcon4bN  30715  ispautN  30896  diaord  31845  dibord  31957  dihord6apre  32054  dihord3  32055  dihord4  32056  dihcnvord  32072  dvh4dimlem  32241  islpolN  32281  mapdordlem2  32435  mapdcnvordN  32456  mapdindp  32469  hdmaplkr  32714
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator