Theorem 3eltr3d 2879

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

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

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 2148  ax-9 2156  ax-ext 2737

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

This theorem is used by:  axcc2lem  10431  axcclem  10452  icoshftf1o  13513  lincmb01cmp  13534  fzosubel  13766  symgsubmefmndALT  19497  psgnunilem1  19587  efgcpbllemb  19849  lspprabs  21246  cnmpt2res  23865  xpstopnlem1  23997  tususp  24459  tustps  24460  ressxms  24713  ressms  24714  tmsxpsval  24726  limcco  26083  dvcnp2  26110  dvmulbr  26129  dvcobr  26136  dvcnvlem  26166  taylthlem2  26568  jensen  27184  f1otrg  29251  nsgqusf1olem1  33762  txomap  34264  probmeasb  34861  fsum2dsub  35035  cvmlift2lem9  35816  nmulel1  36720  nadddilem3  36727  prdsbnd2  38479  iocopn  46269  icoopn  46274  reclimc  46400  cncfiooicclem1  46640  itgiccshift  46727  dirkercncflem4  46853  fourierdlem32  46886  fourierdlem33  46887  fourierdlem60  46913  fourierdlem61  46914  fourierdlem76  46929  fourierdlem81  46934  fourierdlem90  46943  fourierdlem111  46964  uptrlem3  50023  fuco2eld3  50126  fucoid2  50160