Theorem eqriv 2229

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 2226	. 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 1502	1 |- A = B

Syntax hints:   <-> wb 105   = wceq 1398   e. wcel 2203

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 1498  ax-ext 2214

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

This theorem is referenced by:  eqid  2232  sb8ab  2356  cbvabw  2357  cbvab  2358  vjust  2814  nfccdeq  3040  csbcow  3149  difeqri  3339  uneqri  3361  incom  3411  ineqri  3414  difin  3458  invdif  3463  indif  3464  difundi  3473  indifdir  3477  rabsnif  3758  pwv  3913  uniun  3933  intun  3980  intpr  3981  iuncom  3997  iuncom4  3998  iun0  4048  0iun  4049  iunin2  4055  iunun  4070  iunxun  4071  iunxiun  4073  iinpw  4082  inuni  4267  unidif0  4280  unipw  4333  snnex  4569  unon  4633  xpiundi  4808  xpiundir  4809  0xp  4830  iunxpf  4903  cnvuni  4941  dmiun  4965  dmuni  4966  epini  5133  rniun  5173  cnvresima  5252  imaco  5268  rnco  5269  dfmpt3  5481  imaiun  5933  opabex3d  6314  opabex3  6315  ecid  6832  qsid  6834  mapval2  6912  ixpin  6958  dfz2  9650  infssuzex  10593  dfrp2  10623  1nprm  12811  infpn2  13207  rrgval  14407  2idlval  14650  cnfldui  14737  zrhval  14765  plyun0  15601  edgval  16055  clwwlkn0  16403  clwwlknonmpo  16423  clwwlknon  16424  clwwlk0on0  16426