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

Theorem 3sstr4d 3681
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 3667 . 2 (𝜑 → (𝐶𝐷𝐴𝐵))
51, 4mpbird 247 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  suppimacnvss  7350  suppimacnv  7351  ressuppss  7359  suppun  7360  ressuppssdif  7361  suppfnss  7365  suppssov1  7372  suppssfv  7376  omwordri  7697  oewordri  7717  oaabs2  7770  fiss  8371  harword  8511  fin1a2lem12  9271  fzoss1  12534  fzoss2  12535  swrd0  13480  cshimadifsn  13621  trclfvss  13791  trclfvcotrg  13801  relexpnnrn  13829  vdwlem6  15737  vdwlem8  15739  hashbcss  15755  mrcss  16323  gsumzf1o  18359  gsumzaddlem  18367  dprdres  18473  dprdz  18475  dprdf1o  18477  mptscmfsupp0  18976  lspss  19032  lspsntrim  19146  aspss  19380  resspsrbas  19463  resspsradd  19464  resspsrmul  19465  clsss  20906  ntrss  20907  sslm  21151  1stcfb  21296  txss12  21456  prdstopn  21479  imasncls  21543  fmss  21797  flfssfcf  21889  cnpfcfi  21891  ressprdsds  22223  metss2lem  22363  metustto  22405  pi1addval  22894  pi1xfrcnv  22903  equivcau  23144  rrxmvallem  23233  uniiccvol  23394  dyaddisjlem  23409  volsup2  23419  itg2monolem1  23562  itg2gt0  23572  plyss  24000  lgamucov  24809  ifpsnprss  26574  wlkp1lem7  26632  occon  28274  spanss  28335  shlej1  28347  chscllem1  28624  chscllem2  28625  chscllem3  28626  ofrn2  29570  resf1o  29633  fpwrelmap  29636  orvclteinc  30665  dstfrvclim1  30667  reprss  30823  reprinfz1  30828  ss2mcls  31591  noetalem4  31991  heiborlem6  33745  lpssat  34618  lssat  34621  paddass  35442  pclssN  35498  2polssN  35519  polcon3N  35521  paddunN  35531  dibss  36775  dicssdvh  36792  dih2dimb  36850  dih2dimbALTN  36851  dihord5b  36865  dochss  36971  dochspss  36984  dvh3dim3N  37055  lclkrlem2r  37130  lclkr  37139  lclkrs  37145  hgmaprnlem2N  37506  hbtlem4  38013  hbtlem3  38014  itgoss  38050  trrelind  38274  trrelsuperreldg  38277  trrelsuperrel2dg  38280  relexpss1d  38314  trclrelexplem  38320  relexpaddss  38327  frege97d  38361  frege109d  38366  frege131d  38373  clsk1indlem3  38658  limclner  40201  fourierdlem49  40690  fourierdlem92  40733  rngchomfval  42291  rngccofval  42295  rnghmsscmap2  42298  rnghmsscmap  42299  ringchomfval  42337  ringccofval  42341  rhmsscmap2  42344  rhmsscmap  42345  rhmsscrnghm  42351  rngcresringcat  42355  srhmsubc  42401  fldhmsubc  42409  rhmsubclem3  42413  srhmsubcALTV  42419  fldhmsubcALTV  42427  rhmsubcALTVlem4  42432  rmsuppss  42476  mndpsuppss  42477  scmsuppss  42478  setrecsss  42772
  Copyright terms: Public domain W3C validator