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

Theorem 3eltr3d 2846
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 2834 . 2 (𝜑𝐴𝐷)
51, 4eqeltrrd 2833 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809
This theorem is referenced by:  axcc2lem  10413  axcclem  10434  icoshftf1o  13433  lincmb01cmp  13454  fzosubel  13673  symgsubmefmndALT  19235  psgnunilem1  19325  efgcpbllemb  19587  lspprabs  20655  cnmpt2res  23110  xpstopnlem1  23242  tususp  23706  tustps  23707  ressxms  23963  ressms  23964  tmsxpsval  23976  limcco  25339  dvcnp2  25366  dvcnvlem  25422  taylthlem2  25815  jensen  26420  f1otrg  27987  nsgqusf1olem1  32380  txomap  32643  probmeasb  33258  fsum2dsub  33448  cvmlift2lem9  34131  prdsbnd2  36466  iocopn  44004  icoopn  44009  reclimc  44140  cncfiooicclem1  44380  itgiccshift  44467  dirkercncflem4  44593  fourierdlem32  44626  fourierdlem33  44627  fourierdlem60  44653  fourierdlem61  44654  fourierdlem76  44669  fourierdlem81  44674  fourierdlem90  44683  fourierdlem111  44704
  Copyright terms: Public domain W3C validator