Theorem 3eltr3d 2851

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  axcc2lem  10349  axcclem  10370  icoshftf1o  13418  lincmb01cmp  13439  fzosubel  13670  symgsubmefmndALT  19369  psgnunilem1  19459  efgcpbllemb  19721  lspprabs  21082  cnmpt2res  23652  xpstopnlem1  23784  tususp  24246  tustps  24247  ressxms  24500  ressms  24501  tmsxpsval  24513  limcco  25870  dvcnp2  25897  dvmulbr  25916  dvcobr  25923  dvcnvlem  25953  taylthlem2  26351  taylthlem2OLD  26352  jensen  26966  f1otrg  28953  nsgqusf1olem1  33488  txomap  33994  probmeasb  34590  fsum2dsub  34767  cvmlift2lem9  35509  prdsbnd2  38130  iocopn  45968  icoopn  45973  reclimc  46099  cncfiooicclem1  46339  itgiccshift  46426  dirkercncflem4  46552  fourierdlem32  46585  fourierdlem33  46586  fourierdlem60  46612  fourierdlem61  46613  fourierdlem76  46628  fourierdlem81  46633  fourierdlem90  46642  fourierdlem111  46663  uptrlem3  49699  fuco2eld3  49802  fucoid2  49836