Theorem 3eltr3d 2874

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  axcc2lem  10438  axcclem  10459  icoshftf1o  13527  lincmb01cmp  13548  fzosubel  13780  symgsubmefmndALT  19530  psgnunilem1  19620  efgcpbllemb  19882  lspprabs  21279  cnmpt2res  23903  xpstopnlem1  24035  tususp  24497  tustps  24498  ressxms  24751  ressms  24752  tmsxpsval  24764  limcco  26120  dvcnp2  26147  dvmulbr  26166  dvcobr  26173  dvcnvlem  26203  taylthlem2  26610  jensen  27225  f1otrg  29327  nsgqusf1olem1  33842  txomap  34344  probmeasb  34941  fsum2dsub  35115  cvmlift2lem9  35890  nmulel1  36795  nadddilem3  36802  prdsbnd2  38545  iocopn  46350  icoopn  46355  reclimc  46481  cncfiooicclem1  46721  itgiccshift  46808  dirkercncflem4  46934  fourierdlem32  46967  fourierdlem33  46968  fourierdlem60  46994  fourierdlem61  46995  fourierdlem76  47010  fourierdlem81  47015  fourierdlem90  47024  fourierdlem111  47045  uptrlem3  50138  fuco2eld3  50241  fucoid2  50275