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

Theorem 3eltr3d 2864
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 2852 . 2 (𝜑𝐴𝐷)
51, 4eqeltrrd 2851 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-clel 2767
This theorem is referenced by:  axcc2lem  9464  axcclem  9485  icoshftf1o  12502  lincmb01cmp  12522  fzosubel  12735  psgnunilem1  18120  efgcpbllemb  18375  lspprabs  19308  cnmpt2res  21701  xpstopnlem1  21833  tususp  22296  tustps  22297  ressxms  22550  ressms  22551  tmsxpsval  22563  limcco  23877  dvcnp2  23903  dvcnvlem  23959  taylthlem2  24348  jensen  24936  f1otrg  25972  txomap  30241  probmeasb  30832  fsum2dsub  31025  cvmlift2lem9  31631  prdsbnd2  33926  iocopn  40262  icoopn  40267  reclimc  40400  cncfiooicclem1  40621  itgiccshift  40710  dirkercncflem4  40837  fourierdlem32  40870  fourierdlem33  40871  fourierdlem60  40897  fourierdlem61  40898  fourierdlem76  40913  fourierdlem81  40918  fourierdlem90  40927  fourierdlem111  40948
  Copyright terms: Public domain W3C validator