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

Theorem sseq12d 3207
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 3205 . 2  |-  ( ph  ->  ( A  C_  C  <->  B 
C_  C ) )
3 sseq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43sseq2d 3206 . 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 1623    C_ wss 3152
This theorem is referenced by:  3sstr3d  3220  3sstr4d  3221  ssdifeq0  3536  relcnvtr  5192  knatar  5857  smogt  6384  oawordri  6548  omwordi  6569  omwordri  6570  oewordi  6589  oewordri  6590  oeworde  6591  nnawordi  6619  nnmwordi  6633  nnmwordri  6634  sbthlem2  6972  sbth  6981  marypha2lem3  7190  hartogslem1  7257  inf3lem1  7329  tcrank  7554  alephle  7715  cfsmolem  7896  isfin3ds  7955  fin23lem17  7964  fin23lem39  7976  isf32lem1  7979  isf32lem2  7980  isf32lem11  7989  isf33lem  7992  isf34lem7  8005  isf34lem6  8006  fin1a2lem13  8038  itunitc1  8046  dominf  8071  dcomex  8073  axdc2lem  8074  dominfac  8195  fpwwe2cbv  8252  fpwwe2lem2  8254  fpwwecbv  8266  fpwwelem  8267  canthwelem  8272  canthwe  8273  wunex2  8360  swrdval  11450  vdwpc  13027  vdwlem1  13028  vdwlem6  13033  vdwlem7  13034  vdwlem8  13035  isstruct2  13157  ressval  13195  mreexexlemd  13546  isacs1i  13559  isssc  13697  ssc2  13699  fullfunc  13780  fthfunc  13781  isps  14311  istsr  14326  isdir  14354  gsumvalx  14451  efgi2  15034  dmdprd  15236  dprdss  15264  dmdprdpr  15284  basis1  16688  baspartn  16692  eltg  16695  cncls  17003  ispnrm  17067  1stcfb  17171  2ndcctbss  17181  1stcelcls  17187  subislly  17207  kgenidm  17242  ptpjpre1  17266  txcmplem2  17336  flimval  17658  flimcf  17677  fclscf  17720  metss  18054  isngp  18118  iscph  18606  equivcau  18726  caubl  18733  caublcls  18734  ovoliunlem3  18863  volsuplem  18912  volsup  18913  dyaddisj  18951  itg1climres  19069  issh  21787  isch  21802  hsupss  21920  shslej  21959  shlub  21993  ledi  22119  pjoi0  22296  mdbr4  22878  dmdbr4  22886  dmdi4  22887  dmdbr5  22888  mdslle1i  22897  mdslle2i  22898  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd1lem3  22907  mdslmd1lem4  22908  mdslmd1i  22909  sumdmdlem2  22999  sbcss12g  23141  cvmliftlem3  23818  dfrtrcl2  24045  fil2ss  25557  segline  26141  segray  26155  rayline  26156  ismrcd1  26773  ismrcd2  26774  ismrc  26776  incssnn0  26786  diophrw  26838  hbtlem5  27332  hbt  27334  lssatle  29205  pmaple  29950  2polcon4bN  30107  ispautN  30288  diaord  31237  dibord  31349  dihord6apre  31446  dihord3  31447  dihord4  31448  dihcnvord  31464  dvh4dimlem  31633  islpolN  31673  mapdordlem2  31827  mapdcnvordN  31848  mapdindp  31861  hdmaplkr  32106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator