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

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   e. wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used 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  3778  pwv  3934  uniun  3954  intun  4001  intpr  4002  iuncom  4018  iuncom4  4019  iun0  4069  0iun  4070  iunin2  4076  iunun  4091  iunxun  4092  iunxiun  4094  iinpw  4103  inuni  4291  unidif0  4304  unipw  4357  snnex  4594  unon  4658  xpiundi  4833  xpiundir  4834  0xp  4855  iunxpf  4928  cnvuni  4966  dmiun  4990  dmuni  4991  epini  5158  rniun  5198  cnvresima  5277  imaco  5293  rnco  5294  dfmpt3  5506  imaiun  5966  opabex3d  6350  opabex3  6351  ecid  6872  qsid  6874  mapval2  6959  ixpin  7005  dfz2  9722  infssuzex  10677  dfrp2  10709  1nprm  12911  infpn2  13399  cntrval  14145  mgpplusg  14313  mgpbas  14316  ringidval  14356  rrgval  14661  2idlval  14930  cnfldui  15015  zrhval  15043  asclfval  15112  plyun0  15936  edgval  16480  clwwlkn0  16828  clwwlknonmpo  16848  clwwlknon  16849  clwwlk0on0  16851