Theorem 3eltr4g 2923

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	syl5eqel 2910	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐵)
4		3eltr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	syl6eleqr 2917	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   = wceq 1656   ∈ wcel 2164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-clel 2821

This theorem is referenced by:  riotacl2  6884  rankelun  9019  rankelpr  9020  rankelop  9021  cdivcncf  23097  rrx0el  23573  itg1addlem4  23872  cxpcn3  24898  bposlem4  25432  mirauto  26003  ldgenpisyslem1  30767  nosepdm  32368  relowlpssretop  33756  mapfzcons  38122  fourierdlem62  41177  fourierdlem63  41178  line2x  43320  line2y  43321