Theorem 3eltr3d 2878

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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

This theorem is used by:  axcc2lem  10553  axcclem  10574  icoshftf1o  13645  lincmb01cmp  13666  fzosubel  13899  symgsubmefmndALT  19668  psgnunilem1  19758  efgcpbllemb  20020  lspprabs  21421  cnmpt2res  24051  xpstopnlem1  24183  tususp  24645  tustps  24646  ressxms  24899  ressms  24900  tmsxpsval  24912  limcco  26268  dvcnp2  26295  dvmulbr  26314  dvcobr  26321  dvcnvlem  26351  taylthlem2  26758  jensen  27373  f1otrg  29505  edompidlem  33960  nsgqusf1olem1  34068  txomap  34577  probmeasb  35173  fsum2dsub  35347  cvmlift2lem9  36284  nmulel1  37179  nadddilem3  37186  prdsbnd2  38995  iocopn  46805  icoopn  46810  reclimc  46936  cncfiooicclem1  47176  itgiccshift  47263  dirkercncflem4  47389  fourierdlem32  47422  fourierdlem33  47423  fourierdlem60  47449  fourierdlem61  47450  fourierdlem76  47465  fourierdlem81  47470  fourierdlem90  47479  fourierdlem111  47500  uptrlem3  50659  fuco2eld3  50768  fucoid2  50802