Theorem eqriv 2235

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 2232	. 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 1506	1 |- A = B

Syntax hints:   <-> wb 105   = wceq 1402   e. wcel 2209

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 1502  ax-ext 2220

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

This theorem is referenced by:  eqid  2238  sb8ab  2362  cbvabw  2363  cbvab  2364  vjust  2822  nfccdeq  3049  csbcow  3158  difeqri  3349  uneqri  3371  incom  3421  ineqri  3424  difin  3468  invdif  3473  indif  3474  difundi  3483  indifdir  3487  rabsnif  3774  pwv  3929  uniun  3949  intun  3996  intpr  3997  iuncom  4013  iuncom4  4014  iun0  4064  0iun  4065  iunin2  4071  iunun  4086  iunxun  4087  iunxiun  4089  iinpw  4098  inuni  4286  unidif0  4299  unipw  4352  snnex  4589  unon  4653  xpiundi  4828  xpiundir  4829  0xp  4850  iunxpf  4923  cnvuni  4961  dmiun  4985  dmuni  4986  epini  5153  rniun  5193  cnvresima  5272  imaco  5288  rnco  5289  dfmpt3  5501  imaiun  5956  opabex3d  6340  opabex3  6341  ecid  6862  qsid  6864  mapval2  6949  ixpin  6995  dfz2  9696  infssuzex  10644  dfrp2  10676  1nprm  12870  infpn2  13325  rrgval  14543  2idlval  14811  cnfldui  14896  zrhval  14924  plyun0  15760  edgval  16215  clwwlkn0  16563  clwwlknonmpo  16583  clwwlknon  16584  clwwlk0on0  16586