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

Step	Hyp	Ref	Expression
1		3eltr3d.2	. 2
2		3eltr3d.1	. . 3
3		3eltr3d.3	. . 3
4	2, 3	eleqtrd 2547	. 2
5	1, 4	eqeltrrd 2546	1

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