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

Theorem 3sstr4d 3507
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 3493 . 2  |-  ( ph  ->  ( C  C_  D  <->  A 
C_  B ) )
51, 4mpbird 235 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  suppimacnvss  6931  suppimacnv  6932  ressuppss  6941  suppun  6942  ressuppssdif  6943  suppfnss  6947  suppssov1  6954  suppssfv  6958  omwordri  7277  oewordri  7297  oaabs2  7350  fiss  7940  harword  8082  fin1a2lem12  8841  fzoss1  11945  fzoss2  11946  swrd0  12778  trclfvss  13056  trclfvcotrg  13066  relexpnnrn  13094  vdwlem6  14921  vdwlem8  14923  hashbcss  14941  mrcss  15507  gsumzf1o  17531  gsumzaddlem  17539  dprdres  17646  dprdz  17648  dprdf1o  17650  mptscmfsupp0  18138  lspss  18192  lspsntrim  18306  aspss  18541  resspsrbas  18624  resspsradd  18625  resspsrmul  18626  clsss  20053  ntrss  20054  sslm  20299  1stcfb  20444  txss12  20604  prdstopn  20627  imasncls  20691  fmss  20945  flfssfcf  21037  cnpfcfi  21039  ressprdsds  21370  metss2lem  21510  metustto  21552  pi1addval  22063  pi1xfrcnv  22072  equivcau  22254  rrxmvallem  22342  uniiccvol  22521  dyaddisjlem  22537  volsup2  22547  itg2monolem1  22692  itg2gt0  22702  plyss  23137  lgamucov  23947  occon  26923  spanss  26984  shlej1  26996  chscllem1  27273  chscllem2  27274  chscllem3  27275  ofrn2  28228  resf1o  28306  fpwrelmap  28309  orvclteinc  29301  dstfrvclim1  29303  ss2mcls  30199  heiborlem6  32059  lpssat  32495  lssat  32498  paddass  33319  pclssN  33375  2polssN  33396  polcon3N  33398  paddunN  33408  dibss  34653  dicssdvh  34670  dih2dimb  34728  dih2dimbALTN  34729  dihord5b  34743  dochss  34849  dochspss  34862  dvh3dim3N  34933  lclkrlem2r  35008  lclkr  35017  lclkrs  35023  hgmaprnlem2N  35384  hbtlem4  35902  hbtlem3  35903  itgoss  35946  trrelind  36114  trrelsuperreldg  36117  trrelsuperrel2dg  36120  relexpss1d  36154  trclrelexplem  36160  relexpaddss  36167  frege97d  36201  frege109d  36206  frege131d  36213  limclner  37549  fourierdlem49  37836  fourierdlem92  37879  rngchomfval  39154  rngccofval  39158  rnghmsscmap2  39161  rnghmsscmap  39162  ringchomfval  39200  ringccofval  39204  rhmsscmap2  39207  rhmsscmap  39208  rhmsscrnghm  39214  rngcresringcat  39218  srhmsubc  39264  fldhmsubc  39272  rhmsubclem3  39276  srhmsubcALTV  39283  fldhmsubcALTV  39291  rhmsubcALTVlem4  39296  rmsuppss  39343  mndpsuppss  39344  scmsuppss  39345
  Copyright terms: Public domain W3C validator