Theorem eqrdv 2203

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 1897	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2199	. 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 1371   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqrdav  2204  eqabdv  2334  csbcomg  3116  csbabg  3155  uneq1  3320  ineq1  3367  difin2  3435  difsn  3770  intmin4  3913  iunconstm  3935  iinconstm  3936  dfiun2g  3959  iindif2m  3995  iinin2m  3996  iunxsng  4003  iunxsngf  4005  iunpw  4527  opthprc  4726  inimasn  5100  dmsnopg  5154  dfco2a  5183  iotaeq  5240  fun11iun  5543  ssimaex  5640  unpreima  5705  respreima  5708  fconstfvm  5802  reldm  6272  rntpos  6343  frecsuclem  6492  iserd  6646  erth  6666  ecidg  6686  mapdm0  6750  map0e  6773  ixpiinm  6811  pw2f1odclem  6931  fifo  7082  ordiso2  7137  ctssdccl  7213  ctssdc  7215  finacn  7316  exmidapne  7372  acnccim  7384  genpassl  7637  genpassu  7638  1idprl  7703  1idpru  7704  sup3exmid  9030  eqreznegel  9735  iccid  10047  fzsplit2  10172  fzsn  10188  fzpr  10199  uzsplit  10214  fzoval  10270  infssuzex  10376  frec2uzrand  10550  bitsmod  12267  bitscmp  12269  divsfval  13160  mhmpropd  13298  eqgid  13562  ghmmhmb  13590  ghmpropd  13619  ablnsg  13670  opprsubgg  13846  opprunitd  13872  unitpropdg  13910  opprsubrngg  13973  subsubrng2  13977  subrngpropd  13978  subsubrg2  14008  subrgpropd  14015  rhmpropd  14016  lssats2  14176  lsspropdg  14193  discld  14608  restsn  14652  restdis  14656  cndis  14713  cnpdis  14714  tx1cn  14741  tx2cn  14742  blpnf  14872  blininf  14896  blres  14906  xmetec  14909  metrest  14978  xmetxpbl  14980  cnbl0  15006  reopnap  15018  bl2ioo  15022  cncfmet  15064  limcdifap  15134  gausslemma2dlem1a  15535