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

Theorem 3eltr3d 2866
 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 2854 . 2 (𝜑𝐴𝐷)
51, 4eqeltrrd 2853 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-clel 2830 This theorem is referenced by:  axcc2lem  9896  axcclem  9917  icoshftf1o  12906  lincmb01cmp  12927  fzosubel  13145  symgsubmefmndALT  18598  psgnunilem1  18688  efgcpbllemb  18948  lspprabs  19935  cnmpt2res  22377  xpstopnlem1  22509  tususp  22973  tustps  22974  ressxms  23227  ressms  23228  tmsxpsval  23240  limcco  24592  dvcnp2  24619  dvcnvlem  24675  taylthlem2  25068  jensen  25673  f1otrg  26764  nsgqusf1olem1  31119  txomap  31305  probmeasb  31916  fsum2dsub  32106  cvmlift2lem9  32789  prdsbnd2  35513  iocopn  42523  icoopn  42528  reclimc  42661  cncfiooicclem1  42901  itgiccshift  42988  dirkercncflem4  43114  fourierdlem32  43147  fourierdlem33  43148  fourierdlem60  43174  fourierdlem61  43175  fourierdlem76  43190  fourierdlem81  43195  fourierdlem90  43204  fourierdlem111  43225
 Copyright terms: Public domain W3C validator