Theorem eqrdv 2137

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 1846	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2133	. 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 1329   = wceq 1331   e. wcel 1480

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 1423  ax-gen 1425  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  eqrdav  2138  csbcomg  3025  csbabg  3061  uneq1  3223  ineq1  3270  difin2  3338  difsn  3657  intmin4  3799  iunconstm  3821  iinconstm  3822  dfiun2g  3845  iindif2m  3880  iinin2m  3881  iunxsng  3888  iunxsngf  3890  iunpw  4401  opthprc  4590  inimasn  4956  dmsnopg  5010  dfco2a  5039  iotaeq  5096  fun11iun  5388  ssimaex  5482  unpreima  5545  respreima  5548  fconstfvm  5638  reldm  6084  rntpos  6154  frecsuclem  6303  iserd  6455  erth  6473  ecidg  6493  mapdm0  6557  map0e  6580  ixpiinm  6618  fifo  6868  ordiso2  6920  ctssdccl  6996  ctssdc  6998  genpassl  7332  genpassu  7333  1idprl  7398  1idpru  7399  sup3exmid  8715  eqreznegel  9406  iccid  9708  fzsplit2  9830  fzsn  9846  fzpr  9857  uzsplit  9872  fzoval  9925  frec2uzrand  10178  infssuzex  11642  discld  12305  restsn  12349  restdis  12353  cndis  12410  cnpdis  12411  tx1cn  12438  tx2cn  12439  blpnf  12569  blininf  12593  blres  12603  xmetec  12606  metrest  12675  xmetxpbl  12677  cnbl0  12703  reopnap  12707  bl2ioo  12711  cncfmet  12748  limcdifap  12800