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

Theorem 3sstr4d 3611
 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 3597 . 2 (𝜑 → (𝐶𝐷𝐴𝐵))
51, 4mpbird 246 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554 This theorem is referenced by:  suppimacnvss  7192  suppimacnv  7193  ressuppss  7201  suppun  7202  ressuppssdif  7203  suppfnss  7207  suppssov1  7214  suppssfv  7218  omwordri  7539  oewordri  7559  oaabs2  7612  fiss  8213  harword  8353  fin1a2lem12  9116  fzoss1  12364  fzoss2  12365  swrd0  13286  cshimadifsn  13426  trclfvss  13595  trclfvcotrg  13605  relexpnnrn  13633  vdwlem6  15528  vdwlem8  15530  hashbcss  15546  mrcss  16099  gsumzf1o  18136  gsumzaddlem  18144  dprdres  18250  dprdz  18252  dprdf1o  18254  mptscmfsupp0  18751  lspss  18805  lspsntrim  18919  aspss  19153  resspsrbas  19236  resspsradd  19237  resspsrmul  19238  clsss  20668  ntrss  20669  sslm  20913  1stcfb  21058  txss12  21218  prdstopn  21241  imasncls  21305  fmss  21560  flfssfcf  21652  cnpfcfi  21654  ressprdsds  21986  metss2lem  22126  metustto  22168  pi1addval  22656  pi1xfrcnv  22665  equivcau  22906  rrxmvallem  22995  uniiccvol  23154  dyaddisjlem  23169  volsup2  23179  itg2monolem1  23323  itg2gt0  23333  plyss  23759  lgamucov  24564  occon  27530  spanss  27591  shlej1  27603  chscllem1  27880  chscllem2  27881  chscllem3  27882  ofrn2  28822  resf1o  28893  fpwrelmap  28896  orvclteinc  29864  dstfrvclim1  29866  ss2mcls  30719  heiborlem6  32785  lpssat  33318  lssat  33321  paddass  34142  pclssN  34198  2polssN  34219  polcon3N  34221  paddunN  34231  dibss  35476  dicssdvh  35493  dih2dimb  35551  dih2dimbALTN  35552  dihord5b  35566  dochss  35672  dochspss  35685  dvh3dim3N  35756  lclkrlem2r  35831  lclkr  35840  lclkrs  35846  hgmaprnlem2N  36207  hbtlem4  36715  hbtlem3  36716  itgoss  36752  trrelind  36976  trrelsuperreldg  36979  trrelsuperrel2dg  36982  relexpss1d  37016  trclrelexplem  37022  relexpaddss  37029  frege97d  37063  frege109d  37068  frege131d  37075  clsk1indlem3  37361  limclner  38718  fourierdlem49  39048  fourierdlem92  39091  1wlkvtxeledglem  40827  1wlkp1lem7  40888  rngchomfval  41758  rngccofval  41762  rnghmsscmap2  41765  rnghmsscmap  41766  ringchomfval  41804  ringccofval  41808  rhmsscmap2  41811  rhmsscmap  41812  rhmsscrnghm  41818  rngcresringcat  41822  srhmsubc  41868  fldhmsubc  41876  rhmsubclem3  41880  srhmsubcALTV  41887  fldhmsubcALTV  41895  rhmsubcALTVlem4  41900  rmsuppss  41945  mndpsuppss  41946  scmsuppss  41947
 Copyright terms: Public domain W3C validator