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

Metamath Proof Explorer

Theorem eqrdav

Description: Deduce equality of classes from an equivalence of membership that depends on the membership variable. (Contributed by NM, 7-Nov-2008) (Proof shortened by Wolf Lammen, 19-Nov-2019)

	Ref	Expression
Hypotheses	eqrdav.1	$⊢ (φ \land x \in A) \to x \in C$
	eqrdav.2	$⊢ (φ \land x \in B) \to x \in C$
	eqrdav.3	$⊢ (φ \land x \in C) \to (x \in A \leftrightarrow x \in B)$
Assertion	eqrdav	$⊢ φ \to A = B$

Proof

Step	Hyp	Ref	Expression
1		eqrdav.1	$⊢ (φ \land x \in A) \to x \in C$
2		eqrdav.2	$⊢ (φ \land x \in B) \to x \in C$
3		eqrdav.3	$⊢ (φ \land x \in C) \to (x \in A \leftrightarrow x \in B)$
4	1 2 3	bibiad	$⊢ φ \to (x \in A \leftrightarrow x \in B)$
5	4	eqrdv	$⊢ φ \to A = B$