Theorem 3eltr3d 2853

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814

This theorem is referenced by:  axcc2lem  10474  axcclem  10495  icoshftf1o  13511  lincmb01cmp  13532  fzosubel  13760  symgsubmefmndALT  19436  psgnunilem1  19526  efgcpbllemb  19788  lspprabs  21112  cnmpt2res  23701  xpstopnlem1  23833  tususp  24297  tustps  24298  ressxms  24554  ressms  24555  tmsxpsval  24567  limcco  25943  dvcnp2  25970  dvcnp2OLD  25971  dvmulbr  25990  dvcobr  25998  dvcnvlem  26029  taylthlem2  26431  taylthlem2OLD  26432  jensen  27047  f1otrg  28894  nsgqusf1olem1  33421  txomap  33795  probmeasb  34412  fsum2dsub  34601  cvmlift2lem9  35296  prdsbnd2  37782  iocopn  45473  icoopn  45478  reclimc  45609  cncfiooicclem1  45849  itgiccshift  45936  dirkercncflem4  46062  fourierdlem32  46095  fourierdlem33  46096  fourierdlem60  46122  fourierdlem61  46123  fourierdlem76  46138  fourierdlem81  46143  fourierdlem90  46152  fourierdlem111  46173