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

Theorem 3eltr3d 2702
 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 2690 . 2 (𝜑𝐴𝐷)
51, 4eqeltrrd 2689 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606 This theorem is referenced by:  axcc2lem  9141  axcclem  9162  icoshftf1o  12166  lincmb01cmp  12186  fzosubel  12394  psgnunilem1  17736  efgcpbllemb  17991  lspprabs  18916  cnmpt2res  21290  xpstopnlem1  21422  tususp  21886  tustps  21887  ressxms  22140  ressms  22141  tmsxpsval  22153  limcco  23463  dvcnp2  23489  dvcnvlem  23543  taylthlem2  23932  jensen  24515  f1otrg  25551  txomap  29229  probmeasb  29819  cvmlift2lem9  30547  prdsbnd2  32764  iocopn  38593  icoopn  38598  reclimc  38720  cncfiooicclem1  38779  itgiccshift  38872  dirkercncflem4  38999  fourierdlem32  39032  fourierdlem33  39033  fourierdlem60  39059  fourierdlem61  39060  fourierdlem76  39075  fourierdlem81  39080  fourierdlem90  39089  fourierdlem111  39110
 Copyright terms: Public domain W3C validator