Theorem 3eltr3d 2875

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 2863	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
5	1, 4	eqeltrrd 2862	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  axcc2lem  10507  axcclem  10528  icoshftf1o  13598  lincmb01cmp  13619  fzosubel  13852  symgsubmefmndALT  19610  psgnunilem1  19700  efgcpbllemb  19962  lspprabs  21363  cnmpt2res  23989  xpstopnlem1  24121  tususp  24583  tustps  24584  ressxms  24837  ressms  24838  tmsxpsval  24850  limcco  26206  dvcnp2  26233  dvmulbr  26252  dvcobr  26259  dvcnvlem  26289  taylthlem2  26694  jensen  27309  f1otrg  29441  nsgqusf1olem1  33957  txomap  34459  probmeasb  35055  fsum2dsub  35229  cvmlift2lem9  36055  nmulel1  36944  nadddilem3  36951  prdsbnd2  38709  iocopn  46501  icoopn  46506  reclimc  46632  cncfiooicclem1  46872  itgiccshift  46959  dirkercncflem4  47085  fourierdlem32  47118  fourierdlem33  47119  fourierdlem60  47145  fourierdlem61  47146  fourierdlem76  47161  fourierdlem81  47166  fourierdlem90  47175  fourierdlem111  47196  uptrlem3  50289  fuco2eld3  50392  fucoid2  50426