Theorem 3eltr3d 2715

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  axcc2lem  9258  axcclem  9279  icoshftf1o  12295  lincmb01cmp  12315  fzosubel  12526  psgnunilem1  17913  efgcpbllemb  18168  lspprabs  19095  cnmpt2res  21480  xpstopnlem1  21612  tususp  22076  tustps  22077  ressxms  22330  ressms  22331  tmsxpsval  22343  limcco  23657  dvcnp2  23683  dvcnvlem  23739  taylthlem2  24128  jensen  24715  f1otrg  25751  txomap  29901  probmeasb  30492  fsum2dsub  30685  cvmlift2lem9  31293  prdsbnd2  33594  iocopn  39746  icoopn  39751  reclimc  39885  cncfiooicclem1  40106  itgiccshift  40196  dirkercncflem4  40323  fourierdlem32  40356  fourierdlem33  40357  fourierdlem60  40383  fourierdlem61  40384  fourierdlem76  40399  fourierdlem81  40404  fourierdlem90  40413  fourierdlem111  40434