Theorem eqriv 2202

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 2199	. 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 1476	1 |- A = B

Syntax hints:   <-> wb 105   = 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-gen 1472  ax-ext 2187

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

This theorem is referenced by:  eqid  2205  sb8ab  2327  cbvabw  2328  cbvab  2329  vjust  2773  nfccdeq  2996  csbcow  3104  difeqri  3293  uneqri  3315  incom  3365  ineqri  3366  difin  3410  invdif  3415  indif  3416  difundi  3425  indifdir  3429  pwv  3849  uniun  3869  intun  3916  intpr  3917  iuncom  3933  iuncom4  3934  iun0  3984  0iun  3985  iunin2  3991  iunun  4006  iunxun  4007  iunxiun  4009  iinpw  4018  inuni  4199  unidif0  4211  unipw  4261  snnex  4495  unon  4559  xpiundi  4733  xpiundir  4734  0xp  4755  iunxpf  4826  cnvuni  4864  dmiun  4887  dmuni  4888  epini  5053  rniun  5093  cnvresima  5172  imaco  5188  rnco  5189  dfmpt3  5398  imaiun  5829  opabex3d  6206  opabex3  6207  ecid  6685  qsid  6687  mapval2  6765  ixpin  6810  dfz2  9445  infssuzex  10376  dfrp2  10406  1nprm  12436  infpn2  12827  rrgval  14024  2idlval  14264  cnfldui  14351  zrhval  14379  plyun0  15208