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 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836

This theorem is referenced by:  axcc2lem  10386  axcclem  10407  icoshftf1o  13471  lincmb01cmp  13492  fzosubel  13723  symgsubmefmndALT  19433  psgnunilem1  19523  efgcpbllemb  19785  lspprabs  21149  cnmpt2res  23724  xpstopnlem1  23856  tususp  24318  tustps  24319  ressxms  24572  ressms  24573  tmsxpsval  24585  limcco  25942  dvcnp2  25969  dvmulbr  25988  dvcobr  25995  dvcnvlem  26025  taylthlem2  26424  jensen  27040  f1otrg  29027  nsgqusf1olem1  33559  txomap  34091  probmeasb  34687  fsum2dsub  34861  cvmlift2lem9  35621  prdsbnd2  38254  iocopn  46056  icoopn  46061  reclimc  46187  cncfiooicclem1  46427  itgiccshift  46514  dirkercncflem4  46640  fourierdlem32  46673  fourierdlem33  46674  fourierdlem60  46700  fourierdlem61  46701  fourierdlem76  46716  fourierdlem81  46721  fourierdlem90  46730  fourierdlem111  46751  uptrlem3  49793  fuco2eld3  49896  fucoid2  49930