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 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  axcc2lem  10346  axcclem  10367  icoshftf1o  13390  lincmb01cmp  13411  fzosubel  13640  symgsubmefmndALT  19332  psgnunilem1  19422  efgcpbllemb  19684  lspprabs  21047  cnmpt2res  23621  xpstopnlem1  23753  tususp  24215  tustps  24216  ressxms  24469  ressms  24470  tmsxpsval  24482  limcco  25850  dvcnp2  25877  dvcnp2OLD  25878  dvmulbr  25897  dvcobr  25905  dvcnvlem  25936  taylthlem2  26338  taylthlem2OLD  26339  jensen  26955  f1otrg  28943  nsgqusf1olem1  33494  txomap  33991  probmeasb  34587  fsum2dsub  34764  cvmlift2lem9  35505  prdsbnd2  37996  iocopn  45766  icoopn  45771  reclimc  45897  cncfiooicclem1  46137  itgiccshift  46224  dirkercncflem4  46350  fourierdlem32  46383  fourierdlem33  46384  fourierdlem60  46410  fourierdlem61  46411  fourierdlem76  46426  fourierdlem81  46431  fourierdlem90  46440  fourierdlem111  46461  uptrlem3  49457  fuco2eld3  49560  fucoid2  49594