Theorem 3eltr3d 2702

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  axcc2lem  9141  axcclem  9162  icoshftf1o  12166  lincmb01cmp  12186  fzosubel  12394  psgnunilem1  17736  efgcpbllemb  17991  lspprabs  18916  cnmpt2res  21290  xpstopnlem1  21422  tususp  21886  tustps  21887  ressxms  22140  ressms  22141  tmsxpsval  22153  limcco  23463  dvcnp2  23489  dvcnvlem  23543  taylthlem2  23932  jensen  24515  f1otrg  25551  txomap  29229  probmeasb  29819  cvmlift2lem9  30547  prdsbnd2  32764  iocopn  38593  icoopn  38598  reclimc  38720  cncfiooicclem1  38779  itgiccshift  38872  dirkercncflem4  38999  fourierdlem32  39032  fourierdlem33  39033  fourierdlem60  39059  fourierdlem61  39060  fourierdlem76  39075  fourierdlem81  39080  fourierdlem90  39089  fourierdlem111  39110