Theorem 3eltr3d 2846

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809

This theorem is referenced by:  axcc2lem  10413  axcclem  10434  icoshftf1o  13433  lincmb01cmp  13454  fzosubel  13673  symgsubmefmndALT  19235  psgnunilem1  19325  efgcpbllemb  19587  lspprabs  20655  cnmpt2res  23110  xpstopnlem1  23242  tususp  23706  tustps  23707  ressxms  23963  ressms  23964  tmsxpsval  23976  limcco  25339  dvcnp2  25366  dvcnvlem  25422  taylthlem2  25815  jensen  26420  f1otrg  27987  nsgqusf1olem1  32380  txomap  32643  probmeasb  33258  fsum2dsub  33448  cvmlift2lem9  34131  prdsbnd2  36466  iocopn  44004  icoopn  44009  reclimc  44140  cncfiooicclem1  44380  itgiccshift  44467  dirkercncflem4  44593  fourierdlem32  44626  fourierdlem33  44627  fourierdlem60  44653  fourierdlem61  44654  fourierdlem76  44669  fourierdlem81  44674  fourierdlem90  44683  fourierdlem111  44704