Theorem 3eltr3d 2874

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  axcc2lem  10518  axcclem  10539  icoshftf1o  13609  lincmb01cmp  13630  fzosubel  13863  symgsubmefmndALT  19623  psgnunilem1  19713  efgcpbllemb  19975  lspprabs  21376  cnmpt2res  24002  xpstopnlem1  24134  tususp  24596  tustps  24597  ressxms  24850  ressms  24851  tmsxpsval  24863  limcco  26219  dvcnp2  26246  dvmulbr  26265  dvcobr  26272  dvcnvlem  26302  taylthlem2  26707  jensen  27322  f1otrg  29454  nsgqusf1olem1  34011  txomap  34513  probmeasb  35109  fsum2dsub  35283  cvmlift2lem9  36163  nmulel1  37057  nadddilem3  37064  prdsbnd2  38823  iocopn  46626  icoopn  46631  reclimc  46757  cncfiooicclem1  46997  itgiccshift  47084  dirkercncflem4  47210  fourierdlem32  47243  fourierdlem33  47244  fourierdlem60  47270  fourierdlem61  47271  fourierdlem76  47286  fourierdlem81  47291  fourierdlem90  47300  fourierdlem111  47321  uptrlem3  50422  fuco2eld3  50531  fucoid2  50565