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

Theorem 3eltr3d 2924
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 2912 . 2 (𝜑𝐴𝐷)
51, 4eqeltrrd 2911 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  axcc2lem  9846  axcclem  9867  icoshftf1o  12848  lincmb01cmp  12869  fzosubel  13084  psgnunilem1  18550  efgcpbllemb  18810  lspprabs  19796  cnmpt2res  22213  xpstopnlem1  22345  tususp  22808  tustps  22809  ressxms  23062  ressms  23063  tmsxpsval  23075  limcco  24418  dvcnp2  24444  dvcnvlem  24500  taylthlem2  24889  jensen  25493  f1otrg  26584  txomap  30997  probmeasb  31587  fsum2dsub  31777  cvmlift2lem9  32455  prdsbnd2  34954  iocopn  41672  icoopn  41677  reclimc  41810  cncfiooicclem1  42052  itgiccshift  42141  dirkercncflem4  42268  fourierdlem32  42301  fourierdlem33  42302  fourierdlem60  42328  fourierdlem61  42329  fourierdlem76  42344  fourierdlem81  42349  fourierdlem90  42358  fourierdlem111  42379
  Copyright terms: Public domain W3C validator