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

Theorem 3sstr4d 3411
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 3397 . 2  |-  ( ph  ->  ( C  C_  D  <->  A 
C_  B ) )
51, 4mpbird 232 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    C_ wss 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3347  df-ss 3354
This theorem is referenced by:  suppimacnvss  6712  suppimacnv  6713  ressuppss  6720  suppun  6721  ressuppssdif  6722  suppfnss  6726  suppssov1  6733  suppssfv  6737  omwordri  7023  oewordri  7043  oaabs2  7096  fiss  7686  harword  7792  fin1a2lem12  8592  fzoss1  11588  fzoss2  11589  swrd0  12339  vdwlem6  14059  vdwlem8  14061  hashbcss  14077  mrcss  14566  gsumzf1o  16403  gsumzaddlem  16420  dprdres  16537  dprdz  16539  dprdf1o  16541  mptscmfsupp0  17023  lspss  17077  lspsntrim  17191  aspss  17415  resspsrbas  17499  resspsradd  17500  resspsrmul  17501  clsss  18670  ntrss  18671  sslm  18915  1stcfb  19061  txss12  19190  prdstopn  19213  imasncls  19277  fmss  19531  flfssfcf  19623  cnpfcfi  19625  ressprdsds  19958  metss2lem  20098  metusttoOLD  20144  metustto  20145  pi1addval  20632  pi1xfrcnv  20641  equivcau  20823  rrxmvallem  20915  uniiccvol  21072  dyaddisjlem  21087  volsup2  21097  itg2monolem1  21240  itg2gt0  21250  plyss  21679  occon  24702  spanss  24763  shlej1  24775  chscllem1  25052  chscllem2  25053  chscllem3  25054  ofrn2  25970  resf1o  26042  orvclteinc  26870  dstfrvclim1  26872  lgamucov  27036  heiborlem6  28727  hbtlem4  29494  hbtlem3  29495  itgoss  29532  rmsuppss  30795  mndpsuppss  30796  scmsuppss  30797  lpssat  32670  lssat  32673  paddass  33494  pclssN  33550  2polssN  33571  polcon3N  33573  paddunN  33583  dibss  34826  dicssdvh  34843  dih2dimb  34901  dih2dimbALTN  34902  dihord5b  34916  dochss  35022  dochspss  35035  dvh3dim3N  35106  lclkrlem2r  35181  lclkr  35190  lclkrs  35196  hgmaprnlem2N  35557
  Copyright terms: Public domain W3C validator