Theorem 3eltr4g 2852

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  riotacl2  7383  rankelun  9891  rankelpr  9892  rankelop  9893  cdivcncf  24870  rrx0el  25355  itg1addlem4  25657  cxpcn3  26715  bposlem4  27255  nosepdm  27653  mirauto  28668  ldgenpisyslem1  34199  weiunfrlem  36487  relowlpssretop  37387  0prjspnlem  42621  mapfzcons  42714  fourierdlem62  46177  fourierdlem63  46178  gpgprismgr4cycllem8  48081  line2x  48714  line2y  48715