Theorem 3eltr4d

Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	3eltr4d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	3eltr4d.2	⊢ ( 𝜑 → 𝐶 = 𝐴 )
	3eltr4d.3	⊢ ( 𝜑 → 𝐷 = 𝐵 )
Assertion	3eltr4d	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		3eltr4d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2		3eltr4d.2	⊢ ( 𝜑 → 𝐶 = 𝐴 )
3		3eltr4d.3	⊢ ( 𝜑 → 𝐷 = 𝐵 )
4	1 3	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
5	2 4	eqeltrd	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )