Theorem eqriv 2037

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 2034	. 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 1342	1 |- A = B

Syntax hints:   <-> wb 98   = wceq 1243   e. wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  eqid  2040  sb8ab  2159  cbvab  2160  vjust  2558  nfccdeq  2762  difeqri  3064  uneqri  3085  incom  3129  ineqri  3130  difin  3174  invdif  3179  indif  3180  difundi  3189  indifdir  3193  pwv  3579  uniun  3599  intun  3646  intpr  3647  iuncom  3663  iuncom4  3664  iun0  3713  0iun  3714  iunin2  3720  iunun  3734  iunxun  3735  iunxiun  3736  iinpw  3742  inuni  3909  unidif0  3920  unipw  3953  snnex  4181  unon  4237  xpiundi  4398  xpiundir  4399  0xp  4420  iunxpf  4484  cnvuni  4521  dmiun  4544  dmuni  4545  epini  4696  rniun  4734  cnvresima  4810  imaco  4826  rnco  4827  dfmpt3  5021  imaiun  5399  opabex3d  5748  opabex3  5749  ecid  6169  qsid  6171  dfz2  8313