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	3	biimpd	|- ( ( ph /\ x e. C ) -> ( x e. A -> x e. B ) )
5	4	impancom	|- ( ( ph /\ x e. A ) -> ( x e. C -> x e. B ) )
6	1 5	mpd	|- ( ( ph /\ x e. A ) -> x e. B )
7	3	biimprd	|- ( ( ph /\ x e. C ) -> ( x e. B -> x e. A ) )
8	7	impancom	|- ( ( ph /\ x e. B ) -> ( x e. C -> x e. A ) )
9	2 8	mpd	|- ( ( ph /\ x e. B ) -> x e. A )
10	6 9	impbida	|- ( ph -> ( x e. A <-> x e. B ) )
11	10	eqrdv	|- ( ph -> A = B )