Theorem 3eltr3d 2927

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893

This theorem is referenced by:  axcc2lem  9852  axcclem  9873  icoshftf1o  12854  lincmb01cmp  12875  fzosubel  13090  symgsubmefmndALT  18525  psgnunilem1  18615  efgcpbllemb  18875  lspprabs  19861  cnmpt2res  22279  xpstopnlem1  22411  tususp  22875  tustps  22876  ressxms  23129  ressms  23130  tmsxpsval  23142  limcco  24485  dvcnp2  24511  dvcnvlem  24567  taylthlem2  24956  jensen  25560  f1otrg  26651  txomap  31093  probmeasb  31683  fsum2dsub  31873  cvmlift2lem9  32553  prdsbnd2  35067  iocopn  41789  icoopn  41794  reclimc  41927  cncfiooicclem1  42169  itgiccshift  42258  dirkercncflem4  42385  fourierdlem32  42418  fourierdlem33  42419  fourierdlem60  42445  fourierdlem61  42446  fourierdlem76  42461  fourierdlem81  42466  fourierdlem90  42475  fourierdlem111  42496