Theorem eqriv 2154

Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqriv.1	|- ( x e. A <-> x e. B )

Assertion

Ref	Expression
eqriv	|- A = B

Distinct variable groups:   x, A   x, B

Proof of Theorem eqriv

Step	Hyp	Ref	Expression
1		dfcleq 2151	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2		eqriv.1	. 2 |- ( x e. A <-> x e. B )
3	1, 2	mpgbir 1433	1 |- A = B

Syntax hints:   <-> wb 104   = wceq 1335   e. wcel 2128

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-gen 1429  ax-ext 2139

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

This theorem is referenced by:  eqid  2157  sb8ab  2279  cbvabw  2280  cbvab  2281  vjust  2713  nfccdeq  2935  csbcow  3042  difeqri  3227  uneqri  3249  incom  3299  ineqri  3300  difin  3344  invdif  3349  indif  3350  difundi  3359  indifdir  3363  pwv  3771  uniun  3791  intun  3838  intpr  3839  iuncom  3855  iuncom4  3856  iun0  3905  0iun  3906  iunin2  3912  iunun  3927  iunxun  3928  iunxiun  3930  iinpw  3939  inuni  4116  unidif0  4127  unipw  4176  snnex  4406  unon  4468  xpiundi  4641  xpiundir  4642  0xp  4663  iunxpf  4731  cnvuni  4769  dmiun  4792  dmuni  4793  epini  4954  rniun  4993  cnvresima  5072  imaco  5088  rnco  5089  dfmpt3  5289  imaiun  5705  opabex3d  6063  opabex3  6064  ecid  6536  qsid  6538  mapval2  6616  ixpin  6661  dfz2  9219  dfrp2  10145  infssuzex  11817  1nprm  11971