Theorem 3eltr3d 2850

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

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

This theorem is referenced by:  axcc2lem  10358  axcclem  10379  icoshftf1o  13427  lincmb01cmp  13448  fzosubel  13679  symgsubmefmndALT  19378  psgnunilem1  19468  efgcpbllemb  19730  lspprabs  21090  cnmpt2res  23642  xpstopnlem1  23774  tususp  24236  tustps  24237  ressxms  24490  ressms  24491  tmsxpsval  24503  limcco  25860  dvcnp2  25887  dvmulbr  25906  dvcobr  25913  dvcnvlem  25943  taylthlem2  26339  jensen  26952  f1otrg  28939  nsgqusf1olem1  33473  txomap  33978  probmeasb  34574  fsum2dsub  34751  cvmlift2lem9  35493  prdsbnd2  38116  iocopn  45950  icoopn  45955  reclimc  46081  cncfiooicclem1  46321  itgiccshift  46408  dirkercncflem4  46534  fourierdlem32  46567  fourierdlem33  46568  fourierdlem60  46594  fourierdlem61  46595  fourierdlem76  46610  fourierdlem81  46615  fourierdlem90  46624  fourierdlem111  46645  uptrlem3  49687  fuco2eld3  49790  fucoid2  49824