Theorem eqrdv 1473

Description: Deduce equality of classes from equivalence of membership.

Hypothesis

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

Assertion

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

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

Proof of Theorem eqrdv

Step	Hyp	Ref	Expression
1		eqrd.1	. . 3 |- (ph -> (x e. A <-> x e. B))
2	1	19.21aiv 1286	. 2 |- (ph -> A.x(x e. A <-> x e. B))
3		dfcleq 1470	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4	2, 3	sylibr 200	1 |- (ph -> A = B)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956   e. wcel 958

This theorem is referenced by:  csbcomg 2017  uneq1 2177  ineq1 2210  unineq 2255  intmin4 2559  iunconst 2572  iindif2 2611  iununi 2616  iunpw 2914  ordpwsuc 3066  ordsucun 3082  opthprc 3221  imadif 3574  tz6.12-1 3736  ssimaex 3768  fconstfv 3849  funiunfv 3866  2ndconst 4097  erthi 4281  ixp0 4361  pw2en 4446  genpass 5112  1idpr 5133  icounlem 6412  snunioolem 6414  ioojoint 6416  unitgt 7623  tgval3t 7625  clsval2 7685  sncld 7787  cncfmet 7905  bl2ioo 7911  ocin 9169  shscomt 9283  spansncol 9491  rcfpfillem3 10589  rcfpfillem3OLD 10590  iint 10634

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-cleq 1469

Copyright terms: Public domain