Theorem 3eltr3d 2854

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  axcc2lem  10201  axcclem  10222  icoshftf1o  13215  lincmb01cmp  13236  fzosubel  13455  symgsubmefmndALT  19020  psgnunilem1  19110  efgcpbllemb  19370  lspprabs  20366  cnmpt2res  22837  xpstopnlem1  22969  tususp  23433  tustps  23434  ressxms  23690  ressms  23691  tmsxpsval  23703  limcco  25066  dvcnp2  25093  dvcnvlem  25149  taylthlem2  25542  jensen  26147  f1otrg  27241  nsgqusf1olem1  31607  txomap  31793  probmeasb  32406  fsum2dsub  32596  cvmlift2lem9  33282  prdsbnd2  35962  iocopn  43065  icoopn  43070  reclimc  43201  cncfiooicclem1  43441  itgiccshift  43528  dirkercncflem4  43654  fourierdlem32  43687  fourierdlem33  43688  fourierdlem60  43714  fourierdlem61  43715  fourierdlem76  43730  fourierdlem81  43735  fourierdlem90  43744  fourierdlem111  43765