Theorem eqriv 2134

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 2131	. 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 2119

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

This theorem is referenced by:  eqid  2137  sb8ab  2259  cbvabw  2260  cbvab  2261  vjust  2682  nfccdeq  2902  difeqri  3191  uneqri  3213  incom  3263  ineqri  3264  difin  3308  invdif  3313  indif  3314  difundi  3323  indifdir  3327  pwv  3730  uniun  3750  intun  3797  intpr  3798  iuncom  3814  iuncom4  3815  iun0  3864  0iun  3865  iunin2  3871  iunun  3886  iunxun  3887  iunxiun  3889  iinpw  3898  inuni  4075  unidif0  4086  unipw  4134  snnex  4364  unon  4422  xpiundi  4592  xpiundir  4593  0xp  4614  iunxpf  4682  cnvuni  4720  dmiun  4743  dmuni  4744  epini  4905  rniun  4944  cnvresima  5023  imaco  5039  rnco  5040  dfmpt3  5240  imaiun  5654  opabex3d  6012  opabex3  6013  ecid  6485  qsid  6487  mapval2  6565  ixpin  6610  dfz2  9116  infssuzex  11631  1nprm  11784