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

Theorem 3eltr3d 2559
 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 2547 . 2
51, 4eqeltrrd 2546 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818 This theorem is referenced by:  axcc2lem  8837  axcclem  8858  icoshftf1o  11672  lincmb01cmp  11692  fzosubel  11875  psgnunilem1  16518  efgcpbllemb  16773  lspprabs  17741  cnmpt2res  20178  xpstopnlem1  20310  tususp  20775  tustps  20776  ressxms  21028  ressms  21029  tmsxpsval  21041  limcco  22297  dvcnp2  22323  dvcnvlem  22377  taylthlem2  22769  jensen  23318  f1otrg  24174  txomap  27837  probmeasb  28369  cvmlift2lem9  28756  prdsbnd2  30291  iocopn  31560  icoopn  31565  reclimc  31659  cncfiooicclem1  31696  itgiccshift  31779  dirkercncflem4  31888  fourierdlem32  31921  fourierdlem33  31922  fourierdlem60  31949  fourierdlem61  31950  fourierdlem76  31965  fourierdlem81  31970  fourierdlem90  31979  fourierdlem111  32000 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
 Copyright terms: Public domain W3C validator