Theorem 3eltr3d 2899

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

Syntax hints:   → wi 4   = wceq 1525   ∈ wcel 2083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-clel 2865

This theorem is referenced by:  axcc2lem  9711  axcclem  9732  icoshftf1o  12714  lincmb01cmp  12735  fzosubel  12950  psgnunilem1  18356  efgcpbllemb  18612  lspprabs  19561  cnmpt2res  21973  xpstopnlem1  22105  tususp  22568  tustps  22569  ressxms  22822  ressms  22823  tmsxpsval  22835  limcco  24178  dvcnp2  24204  dvcnvlem  24260  taylthlem2  24649  jensen  25252  f1otrg  26344  txomap  30711  probmeasb  31301  fsum2dsub  31491  cvmlift2lem9  32168  prdsbnd2  34626  iocopn  41359  icoopn  41364  reclimc  41497  cncfiooicclem1  41739  itgiccshift  41828  dirkercncflem4  41955  fourierdlem32  41988  fourierdlem33  41989  fourierdlem60  42015  fourierdlem61  42016  fourierdlem76  42031  fourierdlem81  42036  fourierdlem90  42045  fourierdlem111  42066