Theorem 3eltr3d 2848

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  axcc2lem  10450  axcclem  10471  icoshftf1o  13491  lincmb01cmp  13512  fzosubel  13740  symgsubmefmndALT  19384  psgnunilem1  19474  efgcpbllemb  19736  lspprabs  21053  cnmpt2res  23615  xpstopnlem1  23747  tususp  24210  tustps  24211  ressxms  24464  ressms  24465  tmsxpsval  24477  limcco  25846  dvcnp2  25873  dvcnp2OLD  25874  dvmulbr  25893  dvcobr  25901  dvcnvlem  25932  taylthlem2  26334  taylthlem2OLD  26335  jensen  26951  f1otrg  28850  nsgqusf1olem1  33428  txomap  33865  probmeasb  34462  fsum2dsub  34639  cvmlift2lem9  35333  prdsbnd2  37819  iocopn  45549  icoopn  45554  reclimc  45682  cncfiooicclem1  45922  itgiccshift  46009  dirkercncflem4  46135  fourierdlem32  46168  fourierdlem33  46169  fourierdlem60  46195  fourierdlem61  46196  fourierdlem76  46211  fourierdlem81  46216  fourierdlem90  46225  fourierdlem111  46246  fuco2eld3  49226  fucoid2  49260