Theorem eqrdv 2163

Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)

Hypothesis

Ref	Expression
eqrdv.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		eqrdv.1	. . 3 |- ( ph -> ( x e. A <-> x e. B ) )
2	1	alrimiv 1862	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2159	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4	2, 3	sylibr 133	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1341   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  eqrdav  2164  csbcomg  3068  csbabg  3106  uneq1  3269  ineq1  3316  difin2  3384  difsn  3710  intmin4  3852  iunconstm  3874  iinconstm  3875  dfiun2g  3898  iindif2m  3933  iinin2m  3934  iunxsng  3941  iunxsngf  3943  iunpw  4458  opthprc  4655  inimasn  5021  dmsnopg  5075  dfco2a  5104  iotaeq  5161  fun11iun  5453  ssimaex  5547  unpreima  5610  respreima  5613  fconstfvm  5703  reldm  6154  rntpos  6225  frecsuclem  6374  iserd  6527  erth  6545  ecidg  6565  mapdm0  6629  map0e  6652  ixpiinm  6690  fifo  6945  ordiso2  7000  ctssdccl  7076  ctssdc  7078  genpassl  7465  genpassu  7466  1idprl  7531  1idpru  7532  sup3exmid  8852  eqreznegel  9552  iccid  9861  fzsplit2  9985  fzsn  10001  fzpr  10012  uzsplit  10027  fzoval  10083  frec2uzrand  10340  infssuzex  11882  discld  12776  restsn  12820  restdis  12824  cndis  12881  cnpdis  12882  tx1cn  12909  tx2cn  12910  blpnf  13040  blininf  13064  blres  13074  xmetec  13077  metrest  13146  xmetxpbl  13148  cnbl0  13174  reopnap  13178  bl2ioo  13182  cncfmet  13219  limcdifap  13271