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

Theorem 3eltr3d 2855
Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
3eltr3d.1 (𝜑𝐴𝐵)
3eltr3d.2 (𝜑𝐴 = 𝐶)
3eltr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eltr3d (𝜑𝐶𝐷)

Proof of Theorem 3eltr3d
StepHypRef Expression
1 3eltr3d.2 . 2 (𝜑𝐴 = 𝐶)
2 3eltr3d.1 . . 3 (𝜑𝐴𝐵)
3 3eltr3d.3 . . 3 (𝜑𝐵 = 𝐷)
42, 3eleqtrd 2843 . 2 (𝜑𝐴𝐷)
51, 4eqeltrrd 2842 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816
This theorem is referenced by:  axcc2lem  10476  axcclem  10497  icoshftf1o  13514  lincmb01cmp  13535  fzosubel  13763  symgsubmefmndALT  19421  psgnunilem1  19511  efgcpbllemb  19773  lspprabs  21094  cnmpt2res  23685  xpstopnlem1  23817  tususp  24281  tustps  24282  ressxms  24538  ressms  24539  tmsxpsval  24551  limcco  25928  dvcnp2  25955  dvcnp2OLD  25956  dvmulbr  25975  dvcobr  25983  dvcnvlem  26014  taylthlem2  26416  taylthlem2OLD  26417  jensen  27032  f1otrg  28879  nsgqusf1olem1  33441  txomap  33833  probmeasb  34432  fsum2dsub  34622  cvmlift2lem9  35316  prdsbnd2  37802  iocopn  45533  icoopn  45538  reclimc  45668  cncfiooicclem1  45908  itgiccshift  45995  dirkercncflem4  46121  fourierdlem32  46154  fourierdlem33  46155  fourierdlem60  46181  fourierdlem61  46182  fourierdlem76  46197  fourierdlem81  46202  fourierdlem90  46211  fourierdlem111  46232  fuco2eld3  49010  fucoid2  49044
  Copyright terms: Public domain W3C validator