Theorem eqrdav 1883

Description: Deduce equality of classes from an equivalence of membership that depends on the membership variable.

Hypotheses

Ref	Expression
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

Ref	Expression
eqrdav	|- (ph -> A = B)

Distinct variable groups:   x,A   x,B   ph,x

Proof of Theorem eqrdav

Step	Hyp	Ref	Expression
1		eqrdav.1	. . . 4 |- ((ph /\ x e. A) -> x e. C)
2		eqrdav.3	. . . . . . . 8 |- ((ph /\ x e. C) -> (x e. A <-> x e. B))
3	2	biimpd 170	. . . . . . 7 |- ((ph /\ x e. C) -> (x e. A -> x e. B))
4	3	ex 402	. . . . . 6 |- (ph -> (x e. C -> (x e. A -> x e. B)))
5	4	com23 36	. . . . 5 |- (ph -> (x e. A -> (x e. C -> x e. B)))
6	5	imp 377	. . . 4 |- ((ph /\ x e. A) -> (x e. C -> x e. B))
7	1, 6	mpd 29	. . 3 |- ((ph /\ x e. A) -> x e. B)
8		eqrdav.2	. . . 4 |- ((ph /\ x e. B) -> x e. C)
9	2	exbiri 421	. . . . . 6 |- (ph -> (x e. C -> (x e. B -> x e. A)))
10	9	com23 36	. . . . 5 |- (ph -> (x e. B -> (x e. C -> x e. A)))
11	10	imp 377	. . . 4 |- ((ph /\ x e. B) -> (x e. C -> x e. A))
12	8, 11	mpd 29	. . 3 |- ((ph /\ x e. B) -> x e. A)
13	7, 12	impbida 577	. 2 |- (ph -> (x e. A <-> x e. B))
14	13	eqrdv 1882	1 |- (ph -> A = B)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300

This theorem is referenced by:  supminf 13656

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain