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

Theorem sseq12d 3220
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 3218 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
3 sseq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43sseq2d 3219 . 2  |-  ( ph  ->  ( B  C_  C  <->  B 
C_  D ) )
52, 4bitrd 244 1  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    C_ wss 3165
This theorem is referenced by:  3sstr3d  3233  3sstr4d  3234  ssdifeq0  3549  relcnvtr  5208  knatar  5873  smogt  6400  oawordri  6564  omwordi  6585  omwordri  6586  oewordi  6605  oewordri  6606  oeworde  6607  nnawordi  6635  nnmwordi  6649  nnmwordri  6650  sbthlem2  6988  sbth  6997  marypha2lem3  7206  hartogslem1  7273  inf3lem1  7345  tcrank  7570  alephle  7731  cfsmolem  7912  isfin3ds  7971  fin23lem17  7980  fin23lem39  7992  isf32lem1  7995  isf32lem2  7996  isf32lem11  8005  isf33lem  8008  isf34lem7  8021  isf34lem6  8022  fin1a2lem13  8054  itunitc1  8062  dominf  8087  dcomex  8089  axdc2lem  8090  dominfac  8211  fpwwe2cbv  8268  fpwwe2lem2  8270  fpwwecbv  8282  fpwwelem  8283  canthwelem  8288  canthwe  8289  wunex2  8376  swrdval  11466  vdwpc  13043  vdwlem1  13044  vdwlem6  13049  vdwlem7  13050  vdwlem8  13051  isstruct2  13173  ressval  13211  mreexexlemd  13562  isacs1i  13575  isssc  13713  ssc2  13715  fullfunc  13796  fthfunc  13797  isps  14327  istsr  14342  isdir  14370  gsumvalx  14467  efgi2  15050  dmdprd  15252  dprdss  15280  dmdprdpr  15300  basis1  16704  baspartn  16708  eltg  16711  cncls  17019  ispnrm  17083  1stcfb  17187  2ndcctbss  17197  1stcelcls  17203  subislly  17223  kgenidm  17258  ptpjpre1  17282  txcmplem2  17352  flimval  17674  flimcf  17693  fclscf  17736  metss  18070  isngp  18134  iscph  18622  equivcau  18742  caubl  18749  caublcls  18750  ovoliunlem3  18879  volsuplem  18928  volsup  18929  dyaddisj  18967  itg1climres  19085  issh  21803  isch  21818  hsupss  21936  shslej  21975  shlub  22009  ledi  22135  pjoi0  22312  mdbr4  22894  dmdbr4  22902  dmdi4  22903  dmdbr5  22904  mdslle1i  22913  mdslle2i  22914  mdslmd1lem1  22921  mdslmd1lem2  22922  mdslmd1lem3  22923  mdslmd1lem4  22924  mdslmd1i  22925  sumdmdlem2  23015  sbcss12g  23157  cvmliftlem3  23833  dfrtrcl2  24060  fil2ss  25660  segline  26244  segray  26258  rayline  26259  ismrcd1  26876  ismrcd2  26877  ismrc  26879  incssnn0  26889  diophrw  26941  hbtlem5  27435  hbt  27437  lssatle  29827  pmaple  30572  2polcon4bN  30729  ispautN  30910  diaord  31859  dibord  31971  dihord6apre  32068  dihord3  32069  dihord4  32070  dihcnvord  32086  dvh4dimlem  32255  islpolN  32295  mapdordlem2  32449  mapdcnvordN  32470  mapdindp  32483  hdmaplkr  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator