Theorem 3eltr3d 2883

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  axcc2lem  10416  axcclem  10437  icoshftf1o  13497  lincmb01cmp  13518  fzosubel  13749  symgsubmefmndALT  19469  psgnunilem1  19559  efgcpbllemb  19821  lspprabs  21190  cnmpt2res  23799  xpstopnlem1  23931  tususp  24393  tustps  24394  ressxms  24647  ressms  24648  tmsxpsval  24660  limcco  26017  dvcnp2  26044  dvmulbr  26063  dvcobr  26070  dvcnvlem  26100  taylthlem2  26499  jensen  27115  f1otrg  29157  nsgqusf1olem1  33662  txomap  34165  probmeasb  34761  fsum2dsub  34935  cvmlift2lem9  35698  prdsbnd2  38329  iocopn  46121  icoopn  46126  reclimc  46252  cncfiooicclem1  46492  itgiccshift  46579  dirkercncflem4  46705  fourierdlem32  46738  fourierdlem33  46739  fourierdlem60  46765  fourierdlem61  46766  fourierdlem76  46781  fourierdlem81  46786  fourierdlem90  46795  fourierdlem111  46816  uptrlem3  49868  fuco2eld3  49971  fucoid2  50005