Theorem eqrdv 2194

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 1888	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2190	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4	2, 3	sylibr 134	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1362   = wceq 1364   e. wcel 2167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189

This theorem is referenced by:  eqrdav  2195  eqabdv  2325  csbcomg  3107  csbabg  3146  uneq1  3311  ineq1  3358  difin2  3426  difsn  3760  intmin4  3903  iunconstm  3925  iinconstm  3926  dfiun2g  3949  iindif2m  3985  iinin2m  3986  iunxsng  3993  iunxsngf  3995  iunpw  4516  opthprc  4715  inimasn  5088  dmsnopg  5142  dfco2a  5171  iotaeq  5228  fun11iun  5528  ssimaex  5625  unpreima  5690  respreima  5693  fconstfvm  5783  reldm  6253  rntpos  6324  frecsuclem  6473  iserd  6627  erth  6647  ecidg  6667  mapdm0  6731  map0e  6754  ixpiinm  6792  pw2f1odclem  6904  fifo  7055  ordiso2  7110  ctssdccl  7186  ctssdc  7188  finacn  7287  exmidapne  7343  acnccim  7355  genpassl  7608  genpassu  7609  1idprl  7674  1idpru  7675  sup3exmid  9001  eqreznegel  9705  iccid  10017  fzsplit2  10142  fzsn  10158  fzpr  10169  uzsplit  10184  fzoval  10240  infssuzex  10340  frec2uzrand  10514  bitsmod  12138  bitscmp  12140  divsfval  13030  mhmpropd  13168  eqgid  13432  ghmmhmb  13460  ghmpropd  13489  ablnsg  13540  opprsubgg  13716  opprunitd  13742  unitpropdg  13780  opprsubrngg  13843  subsubrng2  13847  subrngpropd  13848  subsubrg2  13878  subrgpropd  13885  rhmpropd  13886  lssats2  14046  lsspropdg  14063  discld  14456  restsn  14500  restdis  14504  cndis  14561  cnpdis  14562  tx1cn  14589  tx2cn  14590  blpnf  14720  blininf  14744  blres  14754  xmetec  14757  metrest  14826  xmetxpbl  14828  cnbl0  14854  reopnap  14866  bl2ioo  14870  cncfmet  14912  limcdifap  14982  gausslemma2dlem1a  15383