Theorem 3eltr3d 2847

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808

This theorem is referenced by:  axcc2lem  10336  axcclem  10357  icoshftf1o  13378  lincmb01cmp  13399  fzosubel  13628  symgsubmefmndALT  19319  psgnunilem1  19409  efgcpbllemb  19671  lspprabs  21033  cnmpt2res  23595  xpstopnlem1  23727  tususp  24189  tustps  24190  ressxms  24443  ressms  24444  tmsxpsval  24456  limcco  25824  dvcnp2  25851  dvcnp2OLD  25852  dvmulbr  25871  dvcobr  25879  dvcnvlem  25910  taylthlem2  26312  taylthlem2OLD  26313  jensen  26929  f1otrg  28852  nsgqusf1olem1  33387  txomap  33870  probmeasb  34466  fsum2dsub  34643  cvmlift2lem9  35378  prdsbnd2  37858  iocopn  45647  icoopn  45652  reclimc  45778  cncfiooicclem1  46018  itgiccshift  46105  dirkercncflem4  46231  fourierdlem32  46264  fourierdlem33  46265  fourierdlem60  46291  fourierdlem61  46292  fourierdlem76  46307  fourierdlem81  46312  fourierdlem90  46321  fourierdlem111  46342  uptrlem3  49340  fuco2eld3  49443  fucoid2  49477