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

Metamath Proof Explorer

Theorem eleq1d

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993) Allow shortening of eleq1 . (Revised by Wolf Lammen, 20-Nov-2019)

		Ref	Expression
	Hypothesis	eleq1d.1	$⊢ φ \to A = B$
	Assertion	eleq1d	$⊢ φ \to (A \in C \leftrightarrow B \in C)$

Proof

Step	Hyp	Ref	Expression
1		eleq1d.1	$⊢ φ \to A = B$
2	1	eqeq2d	$⊢ φ \to (x = A \leftrightarrow x = B)$
3	2	anbi1d	$⊢ φ \to ((x = A \land x \in C) \leftrightarrow (x = B \land x \in C))$
4	3	exbidv	$⊢ φ \to (\exists x (x = A \land x \in C) \leftrightarrow \exists x (x = B \land x \in C))$
5		dfclel	$⊢ A \in C \leftrightarrow \exists x (x = A \land x \in C)$
6		dfclel	$⊢ B \in C \leftrightarrow \exists x (x = B \land x \in C)$
7	4 5 6	3bitr4g	$⊢ φ \to (A \in C \leftrightarrow B \in C)$