Theorem eqriv 2136

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 2133	. 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 1429	1 |- A = B

Syntax hints:   <-> wb 104   = wceq 1331   e. wcel 1480

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 1425  ax-ext 2121

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

This theorem is referenced by:  eqid  2139  sb8ab  2261  cbvabw  2262  cbvab  2263  vjust  2687  nfccdeq  2907  difeqri  3196  uneqri  3218  incom  3268  ineqri  3269  difin  3313  invdif  3318  indif  3319  difundi  3328  indifdir  3332  pwv  3735  uniun  3755  intun  3802  intpr  3803  iuncom  3819  iuncom4  3820  iun0  3869  0iun  3870  iunin2  3876  iunun  3891  iunxun  3892  iunxiun  3894  iinpw  3903  inuni  4080  unidif0  4091  unipw  4139  snnex  4369  unon  4427  xpiundi  4597  xpiundir  4598  0xp  4619  iunxpf  4687  cnvuni  4725  dmiun  4748  dmuni  4749  epini  4910  rniun  4949  cnvresima  5028  imaco  5044  rnco  5045  dfmpt3  5245  imaiun  5661  opabex3d  6019  opabex3  6020  ecid  6492  qsid  6494  mapval2  6572  ixpin  6617  dfz2  9123  infssuzex  11642  1nprm  11795