Theorem eqriv 2193

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 2190	. 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 1467	1 |- A = B

Syntax hints:   <-> wb 105   = wceq 1364   e. wcel 2167

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 1463  ax-ext 2178

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

This theorem is referenced by:  eqid  2196  sb8ab  2318  cbvabw  2319  cbvab  2320  vjust  2764  nfccdeq  2987  csbcow  3095  difeqri  3283  uneqri  3305  incom  3355  ineqri  3356  difin  3400  invdif  3405  indif  3406  difundi  3415  indifdir  3419  pwv  3838  uniun  3858  intun  3905  intpr  3906  iuncom  3922  iuncom4  3923  iun0  3973  0iun  3974  iunin2  3980  iunun  3995  iunxun  3996  iunxiun  3998  iinpw  4007  inuni  4188  unidif0  4200  unipw  4250  snnex  4483  unon  4547  xpiundi  4721  xpiundir  4722  0xp  4743  iunxpf  4814  cnvuni  4852  dmiun  4875  dmuni  4876  epini  5040  rniun  5080  cnvresima  5159  imaco  5175  rnco  5176  dfmpt3  5380  imaiun  5807  opabex3d  6178  opabex3  6179  ecid  6657  qsid  6659  mapval2  6737  ixpin  6782  dfz2  9398  infssuzex  10323  dfrp2  10353  1nprm  12282  infpn2  12673  rrgval  13818  2idlval  14058  cnfldui  14145  zrhval  14173  plyun0  14972