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

Theorem 3sstr4d 3221
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 3207 . 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 1623    C_ wss 3152
This theorem is referenced by:  omwordri  6570  oewordri  6590  oaabs2  6643  fiss  7177  harword  7279  fin1a2lem12  8037  fzoss1  10896  fzoss2  10897  vdwlem6  13033  vdwlem8  13035  hashbcss  13051  mrcss  13518  dprdres  15263  dprdz  15265  dprdf1o  15267  lspss  15741  lspsntrim  15851  aspss  16072  resspsrbas  16159  resspsradd  16160  resspsrmul  16161  clsss  16791  ntrss  16792  sslm  17027  1stcfb  17171  txss12  17300  prdstopn  17322  fmss  17641  flfssfcf  17733  cnpfcfi  17735  ressprdsds  17935  metss2lem  18057  pi1addval  18546  pi1xfrcnv  18555  equivcau  18726  uniiccvol  18935  dyaddisjlem  18950  volsup2  18960  itg2monolem1  19105  itg2gt0  19115  plyss  19581  occon  21866  spanss  21927  shlej1  21939  chscllem1  22216  chscllem2  22217  chscllem3  22218  orvclteinc  23676  dstfrvclim1  23678  islimrs3  25581  islimrs4  25582  dualalg  25782  heiborlem6  26540  hbtlem4  27330  hbtlem3  27331  itgoss  27368  lpssat  29203  lssat  29206  paddass  30027  pclssN  30083  2polssN  30104  polcon3N  30106  paddunN  30116  dibss  31359  dicssdvh  31376  dih2dimb  31434  dih2dimbALTN  31435  dihord5b  31449  dochss  31555  dochspss  31568  dvh3dim3N  31639  lclkrlem2r  31714  lclkr  31723  lclkrs  31729  hgmaprnlem2N  32090
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