This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eleq2d

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019)

		Ref	Expression
	Hypothesis	eleq1d.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	Assertion	eleq2d	⊢ ( 𝜑 → ( 𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1d.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		dfcleq	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
3	1 2	sylib	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
4		anbi2	⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) )
5	4	alexbii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) )
6	3 5	syl	⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) )
7		dfclel	⊢ ( 𝐶 ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) )
8		dfclel	⊢ ( 𝐶 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) )
9	6 7 8	3bitr4g	⊢ ( 𝜑 → ( 𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵 ) )