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	3	biimpd	$⊢ (φ \land x \in C) \to (x \in A \to x \in B)$
5	4	impancom	$⊢ (φ \land x \in A) \to (x \in C \to x \in B)$
6	1 5	mpd	$⊢ (φ \land x \in A) \to x \in B$
7	3	biimprd	$⊢ (φ \land x \in C) \to (x \in B \to x \in A)$
8	7	impancom	$⊢ (φ \land x \in B) \to (x \in C \to x \in A)$
9	2 8	mpd	$⊢ (φ \land x \in B) \to x \in A$
10	6 9	impbida	$⊢ φ \to (x \in A \leftrightarrow x \in B)$
11	10	eqrdv	$⊢ φ \to A = B$