Theorem eqriv 2174

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 2171	. 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 1453	1 |- A = B

Syntax hints:   <-> wb 105   = wceq 1353   e. wcel 2148

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 1449  ax-ext 2159

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

This theorem is referenced by:  eqid  2177  sb8ab  2299  cbvabw  2300  cbvab  2301  vjust  2740  nfccdeq  2962  csbcow  3070  difeqri  3257  uneqri  3279  incom  3329  ineqri  3330  difin  3374  invdif  3379  indif  3380  difundi  3389  indifdir  3393  pwv  3810  uniun  3830  intun  3877  intpr  3878  iuncom  3894  iuncom4  3895  iun0  3945  0iun  3946  iunin2  3952  iunun  3967  iunxun  3968  iunxiun  3970  iinpw  3979  inuni  4157  unidif0  4169  unipw  4219  snnex  4450  unon  4512  xpiundi  4686  xpiundir  4687  0xp  4708  iunxpf  4777  cnvuni  4815  dmiun  4838  dmuni  4839  epini  5001  rniun  5041  cnvresima  5120  imaco  5136  rnco  5137  dfmpt3  5340  imaiun  5763  opabex3d  6124  opabex3  6125  ecid  6600  qsid  6602  mapval2  6680  ixpin  6725  dfz2  9327  dfrp2  10266  infssuzex  11952  1nprm  12116  infpn2  12459