Theorem 3eltr3d 2866

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-clel 2830

This theorem is referenced by:  axcc2lem  9896  axcclem  9917  icoshftf1o  12906  lincmb01cmp  12927  fzosubel  13145  symgsubmefmndALT  18598  psgnunilem1  18688  efgcpbllemb  18948  lspprabs  19935  cnmpt2res  22377  xpstopnlem1  22509  tususp  22973  tustps  22974  ressxms  23227  ressms  23228  tmsxpsval  23240  limcco  24592  dvcnp2  24619  dvcnvlem  24675  taylthlem2  25068  jensen  25673  f1otrg  26764  nsgqusf1olem1  31119  txomap  31305  probmeasb  31916  fsum2dsub  32106  cvmlift2lem9  32789  prdsbnd2  35513  iocopn  42523  icoopn  42528  reclimc  42661  cncfiooicclem1  42901  itgiccshift  42988  dirkercncflem4  43114  fourierdlem32  43147  fourierdlem33  43148  fourierdlem60  43174  fourierdlem61  43175  fourierdlem76  43190  fourierdlem81  43195  fourierdlem90  43204  fourierdlem111  43225