Theorem 3eltr4g 2879

Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypotheses

Ref	Expression
3eltr4g.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
3eltr4g.2	⊢ 𝐶 = 𝐴
3eltr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eltr4g	⊢ (𝜑 → 𝐶 ∈ 𝐷)

Proof of Theorem 3eltr4g

Step	Hyp	Ref	Expression
1		3eltr4g.2	. . 3 ⊢ 𝐶 = 𝐴
2		3eltr4g.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
3	1, 2	eqeltrid 2866	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐵)
4		3eltr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eleqtrrdi 2873	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-clel 2837

This theorem is used by:  riotacl2  7385  rankelun  9842  rankelpr  9843  rankelop  9844  cdivcncf  25091  rrx0el  25568  itg1addlem4  25869  cxpcn3  26924  bposlem4  27462  nosepdm  27859  mirauto  28972  ldgenpisyslem1  34562  weiunfrlem  37003  relowlpssretop  38038  0prjspnlem  43383  mapfzcons  43475  fourierdlem62  46910  fourierdlem63  46911  gpgprismgr4cycllem8  48895  line2x  49562  line2y  49563