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

Theorem 3sstr4d 3547
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 3533 . 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 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  suppimacnvss  6912  suppimacnv  6913  ressuppss  6920  suppun  6921  ressuppssdif  6922  suppfnss  6926  suppssov1  6933  suppssfv  6937  omwordri  7222  oewordri  7242  oaabs2  7295  fiss  7885  harword  7992  fin1a2lem12  8792  fzoss1  11821  fzoss2  11822  swrd0  12624  vdwlem6  14366  vdwlem8  14368  hashbcss  14384  mrcss  14874  gsumzf1o  16732  gsumzaddlem  16749  dprdres  16889  dprdz  16891  dprdf1o  16893  mptscmfsupp0  17388  lspss  17442  lspsntrim  17556  aspss  17792  resspsrbas  17881  resspsradd  17882  resspsrmul  17883  clsss  19361  ntrss  19362  sslm  19606  1stcfb  19752  txss12  19933  prdstopn  19956  imasncls  20020  fmss  20274  flfssfcf  20366  cnpfcfi  20368  ressprdsds  20701  metss2lem  20841  metusttoOLD  20887  metustto  20888  pi1addval  21375  pi1xfrcnv  21384  equivcau  21566  rrxmvallem  21658  uniiccvol  21816  dyaddisjlem  21831  volsup2  21841  itg2monolem1  21984  itg2gt0  21994  plyss  22423  occon  25978  spanss  26039  shlej1  26051  chscllem1  26328  chscllem2  26329  chscllem3  26330  ofrn2  27250  resf1o  27322  orvclteinc  28165  dstfrvclim1  28167  lgamucov  28331  ss2mcls  28679  heiborlem6  30142  hbtlem4  30906  hbtlem3  30907  itgoss  30944  fourierdlem92  31726  rmsuppss  32261  mndpsuppss  32262  scmsuppss  32263  lpssat  34027  lssat  34030  paddass  34851  pclssN  34907  2polssN  34928  polcon3N  34930  paddunN  34940  dibss  36183  dicssdvh  36200  dih2dimb  36258  dih2dimbALTN  36259  dihord5b  36273  dochss  36379  dochspss  36392  dvh3dim3N  36463  lclkrlem2r  36538  lclkr  36547  lclkrs  36553  hgmaprnlem2N  36914  trrelind  37005  trrelsuperreldg  37010
  Copyright terms: Public domain W3C validator