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  4293  unidif0  4306  unipw  4359  snnex  4596  unon  4660  xpiundi  4835  xpiundir  4836  0xp  4857  iunxpf  4930  cnvuni  4968  dmiun  4992  dmuni  4993  epini  5161  rniun  5201  cnvresima  5280  imaco  5296  rnco  5297  dfmpt3  5509  imaiun  5969  opabex3d  6354  opabex3  6355  ecid  6877  qsid  6879  mapval2  6964  ixpin  7011  dfz2  9726  infssuzex  10682  dfrp2  10714  1nprm  12916  infpn2  13404  cntrval  14150  mgpplusg  14328  mgpbas  14331  ringidval  14371  rrgval  14678  2idlval  14947  cnfldui  15032  zrhval  15060  asclfval  15129  mplbas  15223  plyun0  15979  edgval  16523  clwwlkn0  16871  clwwlknonmpo  16891  clwwlknon  16892  clwwlk0on0  16894  idjudju  17269