Theorem eqrdv 2079

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

Syntax hints:   -> wi 4   <-> wb 103   A.wal 1282   = wceq 1284   e. wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  eqrdav  2080  csbcomg  2929  csbabg  2963  uneq1  3119  ineq1  3160  difin2  3226  difsn  3523  intmin4  3664  iunconstm  3686  iinconstm  3687  dfiun2g  3710  iindif2m  3745  iinin2m  3746  iunxsng  3753  iunpw  4229  opthprc  4409  inimasn  4761  dmsnopg  4812  dfco2a  4841  iotaeq  4895  fun11iun  5167  ssimaex  5255  unpreima  5313  respreima  5316  fconstfvm  5400  reldm  5832  rntpos  5895  frecsuclem3  6013  iserd  6155  erth  6173  ecidg  6193  ordiso2  6446  genpassl  6714  genpassu  6715  1idprl  6780  1idpru  6781  eqreznegel  8699  iccid  8948  fzsplit2  9069  fzsn  9084  fzpr  9094  uzsplit  9109  fzoval  9158  frec2uzrand  9407  infssuzex  10345