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

Theorem 3eltr3d 2712
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 2700 . 2 (𝜑𝐴𝐷)
51, 4eqeltrrd 2699 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617
This theorem is referenced by:  axcc2lem  9202  axcclem  9223  icoshftf1o  12237  lincmb01cmp  12257  fzosubel  12467  psgnunilem1  17834  efgcpbllemb  18089  lspprabs  19014  cnmpt2res  21390  xpstopnlem1  21522  tususp  21986  tustps  21987  ressxms  22240  ressms  22241  tmsxpsval  22253  limcco  23563  dvcnp2  23589  dvcnvlem  23643  taylthlem2  24032  jensen  24615  f1otrg  25651  txomap  29683  probmeasb  30273  cvmlift2lem9  31001  prdsbnd2  33226  iocopn  39157  icoopn  39162  reclimc  39289  cncfiooicclem1  39410  itgiccshift  39503  dirkercncflem4  39630  fourierdlem32  39663  fourierdlem33  39664  fourierdlem60  39690  fourierdlem61  39691  fourierdlem76  39706  fourierdlem81  39711  fourierdlem90  39720  fourierdlem111  39741
  Copyright terms: Public domain W3C validator