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 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815

This theorem is referenced by:  axcc2lem  10356  axcclem  10377  icoshftf1o  13425  lincmb01cmp  13446  fzosubel  13677  symgsubmefmndALT  19376  psgnunilem1  19466  efgcpbllemb  19728  lspprabs  21092  cnmpt2res  23667  xpstopnlem1  23799  tususp  24261  tustps  24262  ressxms  24515  ressms  24516  tmsxpsval  24528  limcco  25885  dvcnp2  25912  dvmulbr  25931  dvcobr  25938  dvcnvlem  25968  taylthlem2  26364  jensen  26977  f1otrg  28964  nsgqusf1olem1  33503  txomap  34025  probmeasb  34621  fsum2dsub  34798  cvmlift2lem9  35546  prdsbnd2  38169  iocopn  45972  icoopn  45977  reclimc  46103  cncfiooicclem1  46343  itgiccshift  46430  dirkercncflem4  46556  fourierdlem32  46589  fourierdlem33  46590  fourierdlem60  46616  fourierdlem61  46617  fourierdlem76  46632  fourierdlem81  46637  fourierdlem90  46646  fourierdlem111  46667  uptrlem3  49709  fuco2eld3  49812  fucoid2  49846