Theorem cleqrd 1100

Description: Deduce equality of sets from equivalence of membership.

Hypothesis

Ref	Expression
cleqrd.1	|- (ph -> (x e. A <-> x e. B))

Assertion

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

Distinct variable group(s):   x,A   x,B   ph,x

Proof of Theorem cleqrd

Step	Hyp	Ref	Expression
1		cleqrd.1	. . 3 |- (ph -> (x e. A <-> x e. B))
2	1	19.21aiv 943	. 2 |- (ph -> A.x(x e. A <-> x e. B))
3		dfcleq 1098	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4	2, 3	sylibr 175	1 |- (ph -> A = B)

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672   = wceq 1091   e. wcel 1092

This theorem is referenced by:  uneq1 1605  ineq1 1638  unineq 1680  iunconst 2000  iindif2 2033  iununi 2037  iunpw 2040  onpwsuc 2315  ordsucun 2333  opthprc 2457  imadif 2714  tz6.12-1 2842  fconstfv 2903  erthi 3218  pw2en 3348  genpass 3906  1idpr 3927  ocin 5177  shscomt 5284  spansncol 5473

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-cleq 1097

metamath.org