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

Theorem 3sstr4d 3627
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 (𝜑𝐴𝐵)
3sstr4d.2 (𝜑𝐶 = 𝐴)
3sstr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3sstr4d (𝜑𝐶𝐷)

Proof of Theorem 3sstr4d
StepHypRef Expression
1 3sstr4d.1 . 2 (𝜑𝐴𝐵)
2 3sstr4d.2 . . 3 (𝜑𝐶 = 𝐴)
3 3sstr4d.3 . . 3 (𝜑𝐷 = 𝐵)
42, 3sseq12d 3613 . 2 (𝜑 → (𝐶𝐷𝐴𝐵))
51, 4mpbird 247 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3562  df-ss 3569
This theorem is referenced by:  suppimacnvss  7250  suppimacnv  7251  ressuppss  7259  suppun  7260  ressuppssdif  7261  suppfnss  7265  suppssov1  7272  suppssfv  7276  omwordri  7597  oewordri  7617  oaabs2  7670  fiss  8274  harword  8414  fin1a2lem12  9177  fzoss1  12436  fzoss2  12437  swrd0  13372  cshimadifsn  13512  trclfvss  13681  trclfvcotrg  13691  relexpnnrn  13719  vdwlem6  15614  vdwlem8  15616  hashbcss  15632  mrcss  16197  gsumzf1o  18234  gsumzaddlem  18242  dprdres  18348  dprdz  18350  dprdf1o  18352  mptscmfsupp0  18849  lspss  18903  lspsntrim  19017  aspss  19251  resspsrbas  19334  resspsradd  19335  resspsrmul  19336  clsss  20768  ntrss  20769  sslm  21013  1stcfb  21158  txss12  21318  prdstopn  21341  imasncls  21405  fmss  21660  flfssfcf  21752  cnpfcfi  21754  ressprdsds  22086  metss2lem  22226  metustto  22268  pi1addval  22756  pi1xfrcnv  22765  equivcau  23006  rrxmvallem  23095  uniiccvol  23254  dyaddisjlem  23269  volsup2  23279  itg2monolem1  23423  itg2gt0  23433  plyss  23859  lgamucov  24664  ifpsnprss  26388  wlkp1lem7  26445  occon  27992  spanss  28053  shlej1  28065  chscllem1  28342  chscllem2  28343  chscllem3  28344  ofrn2  29281  resf1o  29345  fpwrelmap  29348  orvclteinc  30315  dstfrvclim1  30317  ss2mcls  31170  heiborlem6  33244  lpssat  33777  lssat  33780  paddass  34601  pclssN  34657  2polssN  34678  polcon3N  34680  paddunN  34690  dibss  35935  dicssdvh  35952  dih2dimb  36010  dih2dimbALTN  36011  dihord5b  36025  dochss  36131  dochspss  36144  dvh3dim3N  36215  lclkrlem2r  36290  lclkr  36299  lclkrs  36305  hgmaprnlem2N  36666  hbtlem4  37174  hbtlem3  37175  itgoss  37211  trrelind  37435  trrelsuperreldg  37438  trrelsuperrel2dg  37441  relexpss1d  37475  trclrelexplem  37481  relexpaddss  37488  frege97d  37522  frege109d  37527  frege131d  37534  clsk1indlem3  37820  limclner  39284  fourierdlem49  39676  fourierdlem92  39719  rngchomfval  41251  rngccofval  41255  rnghmsscmap2  41258  rnghmsscmap  41259  ringchomfval  41297  ringccofval  41301  rhmsscmap2  41304  rhmsscmap  41305  rhmsscrnghm  41311  rngcresringcat  41315  srhmsubc  41361  fldhmsubc  41369  rhmsubclem3  41373  srhmsubcALTV  41379  fldhmsubcALTV  41387  rhmsubcALTVlem4  41392  rmsuppss  41436  mndpsuppss  41437  scmsuppss  41438
  Copyright terms: Public domain W3C validator