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

Theorem 3sstr4d 3234
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
3sstr4d.1  |-  ( ph  ->  A  C_  B )
3sstr4d.2  |-  ( ph  ->  C  =  A )
3sstr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3sstr4d  |-  ( ph  ->  C  C_  D )

Proof of Theorem 3sstr4d
StepHypRef Expression
1 3sstr4d.1 . 2  |-  ( ph  ->  A  C_  B )
2 3sstr4d.2 . . 3  |-  ( ph  ->  C  =  A )
3 3sstr4d.3 . . 3  |-  ( ph  ->  D  =  B )
42, 3sseq12d 3220 . 2  |-  ( ph  ->  ( C  C_  D  <->  A 
C_  B ) )
51, 4mpbird 223 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  omwordri  6586  oewordri  6606  oaabs2  6659  fiss  7193  harword  7295  fin1a2lem12  8053  fzoss1  10912  fzoss2  10913  vdwlem6  13049  vdwlem8  13051  hashbcss  13067  mrcss  13534  dprdres  15279  dprdz  15281  dprdf1o  15283  lspss  15757  lspsntrim  15867  aspss  16088  resspsrbas  16175  resspsradd  16176  resspsrmul  16177  clsss  16807  ntrss  16808  sslm  17043  1stcfb  17187  txss12  17316  prdstopn  17338  fmss  17657  flfssfcf  17749  cnpfcfi  17751  ressprdsds  17951  metss2lem  18073  pi1addval  18562  pi1xfrcnv  18571  equivcau  18742  uniiccvol  18951  dyaddisjlem  18966  volsup2  18976  itg2monolem1  19121  itg2gt0  19131  plyss  19597  occon  21882  spanss  21943  shlej1  21955  chscllem1  22232  chscllem2  22233  chscllem3  22234  orvclteinc  23691  dstfrvclim1  23693  islimrs3  25684  islimrs4  25685  dualalg  25885  heiborlem6  26643  hbtlem4  27433  hbtlem3  27434  itgoss  27471  lpssat  29825  lssat  29828  paddass  30649  pclssN  30705  2polssN  30726  polcon3N  30728  paddunN  30738  dibss  31981  dicssdvh  31998  dih2dimb  32056  dih2dimbALTN  32057  dihord5b  32071  dochss  32177  dochspss  32190  dvh3dim3N  32261  lclkrlem2r  32336  lclkr  32345  lclkrs  32351  hgmaprnlem2N  32712
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