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	$$⊢\left(\phi \wedge x\in A\right)\to x\in C$$
	eqrdav.2	$$⊢\left(\phi \wedge x\in B\right)\to x\in C$$
	eqrdav.3	$$⊢\left(\phi \wedge x\in C\right)\to \left(x\in A\leftrightarrow x\in B\right)$$
Assertion	eqrdav	$$⊢\phi \to A=B$$

Proof

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