Theorem 3sstr4d 3648

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

Step	Hyp	Ref	Expression
1		3sstr4d.1	. 2 |- ( ph -> A C_ B )
2		3sstr4d.2	. . 3 |- ( ph -> C = A )
3		3sstr4d.3	. . 3 |- ( ph -> D = B )
4	2, 3	sseq12d 3634	. 2 |- ( ph -> ( C C_ D <-> A C_ B ) )
5	1, 4	mpbird 247	1 |- ( ph -> C C_ D )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  suppimacnvss  7305  suppimacnv  7306  ressuppss  7314  suppun  7315  ressuppssdif  7316  suppfnss  7320  suppssov1  7327  suppssfv  7331  omwordri  7652  oewordri  7672  oaabs2  7725  fiss  8330  harword  8470  fin1a2lem12  9233  fzoss1  12495  fzoss2  12496  swrd0  13434  cshimadifsn  13575  trclfvss  13747  trclfvcotrg  13757  relexpnnrn  13785  vdwlem6  15690  vdwlem8  15692  hashbcss  15708  mrcss  16276  gsumzf1o  18313  gsumzaddlem  18321  dprdres  18427  dprdz  18429  dprdf1o  18431  mptscmfsupp0  18928  lspss  18984  lspsntrim  19098  aspss  19332  resspsrbas  19415  resspsradd  19416  resspsrmul  19417  clsss  20858  ntrss  20859  sslm  21103  1stcfb  21248  txss12  21408  prdstopn  21431  imasncls  21495  fmss  21750  flfssfcf  21842  cnpfcfi  21844  ressprdsds  22176  metss2lem  22316  metustto  22358  pi1addval  22848  pi1xfrcnv  22857  equivcau  23098  rrxmvallem  23187  uniiccvol  23348  dyaddisjlem  23363  volsup2  23373  itg2monolem1  23517  itg2gt0  23527  plyss  23955  lgamucov  24764  ifpsnprss  26518  wlkp1lem7  26576  occon  28146  spanss  28207  shlej1  28219  chscllem1  28496  chscllem2  28497  chscllem3  28498  ofrn2  29442  resf1o  29505  fpwrelmap  29508  orvclteinc  30537  dstfrvclim1  30539  reprss  30695  reprinfz1  30700  ss2mcls  31465  noetalem4  31866  heiborlem6  33615  lpssat  34300  lssat  34303  paddass  35124  pclssN  35180  2polssN  35201  polcon3N  35203  paddunN  35213  dibss  36458  dicssdvh  36475  dih2dimb  36533  dih2dimbALTN  36534  dihord5b  36548  dochss  36654  dochspss  36667  dvh3dim3N  36738  lclkrlem2r  36813  lclkr  36822  lclkrs  36828  hgmaprnlem2N  37189  hbtlem4  37696  hbtlem3  37697  itgoss  37733  trrelind  37957  trrelsuperreldg  37960  trrelsuperrel2dg  37963  relexpss1d  37997  trclrelexplem  38003  relexpaddss  38010  frege97d  38044  frege109d  38049  frege131d  38056  clsk1indlem3  38341  limclner  39883  fourierdlem49  40372  fourierdlem92  40415  rngchomfval  41966  rngccofval  41970  rnghmsscmap2  41973  rnghmsscmap  41974  ringchomfval  42012  ringccofval  42016  rhmsscmap2  42019  rhmsscmap  42020  rhmsscrnghm  42026  rngcresringcat  42030  srhmsubc  42076  fldhmsubc  42084  rhmsubclem3  42088  srhmsubcALTV  42094  fldhmsubcALTV  42102  rhmsubcALTVlem4  42107  rmsuppss  42151  mndpsuppss  42152  scmsuppss  42153