Theorem 3eltr3d 2855

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816

This theorem is referenced by:  axcc2lem  10476  axcclem  10497  icoshftf1o  13514  lincmb01cmp  13535  fzosubel  13763  symgsubmefmndALT  19421  psgnunilem1  19511  efgcpbllemb  19773  lspprabs  21094  cnmpt2res  23685  xpstopnlem1  23817  tususp  24281  tustps  24282  ressxms  24538  ressms  24539  tmsxpsval  24551  limcco  25928  dvcnp2  25955  dvcnp2OLD  25956  dvmulbr  25975  dvcobr  25983  dvcnvlem  26014  taylthlem2  26416  taylthlem2OLD  26417  jensen  27032  f1otrg  28879  nsgqusf1olem1  33441  txomap  33833  probmeasb  34432  fsum2dsub  34622  cvmlift2lem9  35316  prdsbnd2  37802  iocopn  45533  icoopn  45538  reclimc  45668  cncfiooicclem1  45908  itgiccshift  45995  dirkercncflem4  46121  fourierdlem32  46154  fourierdlem33  46155  fourierdlem60  46181  fourierdlem61  46182  fourierdlem76  46197  fourierdlem81  46202  fourierdlem90  46211  fourierdlem111  46232  fuco2eld3  49010  fucoid2  49044