Theorem 3eltr4g 2856

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

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

This theorem is referenced by:  riotacl2  7404  rankelun  9910  rankelpr  9911  rankelop  9912  cdivcncf  24961  rrx0el  25446  itg1addlem4  25748  itg1addlem4OLD  25749  cxpcn3  26806  bposlem4  27346  nosepdm  27744  mirauto  28707  ldgenpisyslem1  34144  weiunfrlem  36447  relowlpssretop  37347  0prjspnlem  42610  mapfzcons  42704  fourierdlem62  46124  fourierdlem63  46125  line2x  48604  line2y  48605