Theorem 3eltr4g 2858

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 2845	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐵)
4		3eltr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eleqtrrdi 2852	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  riotacl2  7333  rankelun  9791  rankelpr  9792  rankelop  9793  cdivcncf  24910  rrx0el  25387  itg1addlem4  25688  cxpcn3  26734  bposlem4  27272  nosepdm  27670  mirauto  28774  ldgenpisyslem1  34359  weiunfrlem  36707  relowlpssretop  37741  0prjspnlem  43088  mapfzcons  43180  fourierdlem62  46625  fourierdlem63  46626  gpgprismgr4cycllem8  48607  line2x  49259  line2y  49260