Theorem eqriv 2078

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 2075	. 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 1382	1 |- A = B

Syntax hints:   <-> wb 103   = 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-gen 1378  ax-ext 2063

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

This theorem is referenced by:  eqid  2081  sb8ab  2200  cbvab  2201  vjust  2602  nfccdeq  2813  difeqri  3092  uneqri  3114  incom  3158  ineqri  3159  difin  3201  invdif  3206  indif  3207  difundi  3216  indifdir  3220  pwv  3600  uniun  3620  intun  3667  intpr  3668  iuncom  3684  iuncom4  3685  iun0  3734  0iun  3735  iunin2  3741  iunun  3755  iunxun  3756  iunxiun  3757  iinpw  3763  inuni  3930  unidif0  3941  unipw  3972  snnex  4199  unon  4255  xpiundi  4416  xpiundir  4417  0xp  4438  iunxpf  4502  cnvuni  4539  dmiun  4562  dmuni  4563  epini  4716  rniun  4754  cnvresima  4830  imaco  4846  rnco  4847  dfmpt3  5041  imaiun  5420  opabex3d  5768  opabex3  5769  ecid  6192  qsid  6194  dfz2  8420  infssuzex  10345  1nprm  10496