Theorem 3eltr3d

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

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

Proof

Step	Hyp	Ref	Expression
1		3eltr3d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2		3eltr3d.2	⊢ ( 𝜑 → 𝐴 = 𝐶 )
3		3eltr3d.3	⊢ ( 𝜑 → 𝐵 = 𝐷 )
4	1 3	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
5	2 4	eqeltrrd	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )