Theorem 3eltr3d 2851

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  axcc2lem  10358  axcclem  10379  icoshftf1o  13402  lincmb01cmp  13423  fzosubel  13652  symgsubmefmndALT  19344  psgnunilem1  19434  efgcpbllemb  19696  lspprabs  21059  cnmpt2res  23633  xpstopnlem1  23765  tususp  24227  tustps  24228  ressxms  24481  ressms  24482  tmsxpsval  24494  limcco  25862  dvcnp2  25889  dvcnp2OLD  25890  dvmulbr  25909  dvcobr  25917  dvcnvlem  25948  taylthlem2  26350  taylthlem2OLD  26351  jensen  26967  f1otrg  28955  nsgqusf1olem1  33505  txomap  34011  probmeasb  34607  fsum2dsub  34784  cvmlift2lem9  35524  prdsbnd2  38043  iocopn  45877  icoopn  45882  reclimc  46008  cncfiooicclem1  46248  itgiccshift  46335  dirkercncflem4  46461  fourierdlem32  46494  fourierdlem33  46495  fourierdlem60  46521  fourierdlem61  46522  fourierdlem76  46537  fourierdlem81  46542  fourierdlem90  46551  fourierdlem111  46572  uptrlem3  49568  fuco2eld3  49671  fucoid2  49705