Theorem 3eltr4g 2881

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

Syntax hints:   → wi 4   = wceq 1562   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839

This theorem is referenced by:  riotacl2  7371  rankelun  9832  rankelpr  9833  rankelop  9834  cdivcncf  24985  rrx0el  25462  itg1addlem4  25763  cxpcn3  26815  bposlem4  27353  nosepdm  27750  mirauto  28859  ldgenpisyslem1  34462  weiunfrlem  36829  relowlpssretop  37863  0prjspnlem  43210  mapfzcons  43302  fourierdlem62  46747  fourierdlem63  46748  gpgprismgr4cycllem8  48729  line2x  49381  line2y  49382