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	|- ( ( ph /\ x e. A ) -> x e. C )
	eqrdav.2	|- ( ( ph /\ x e. B ) -> x e. C )
	eqrdav.3	|- ( ( ph /\ x e. C ) -> ( x e. A <-> x e. B ) )
Assertion	eqrdav	|- ( ph -> A = B )

Proof

Step	Hyp	Ref	Expression
1		eqrdav.1	|- ( ( ph /\ x e. A ) -> x e. C )
2		eqrdav.2	|- ( ( ph /\ x e. B ) -> x e. C )
3		eqrdav.3	|- ( ( ph /\ x e. C ) -> ( x e. A <-> x e. B ) )
4	1 2 3	bibiad	|- ( ph -> ( x e. A <-> x e. B ) )
5	4	eqrdv	|- ( ph -> A = B )