Theorem eqriv 2226

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 2223	. 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 1499	1 |- A = B

Syntax hints:   <-> wb 105   = wceq 1395   e. wcel 2200

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 1495  ax-ext 2211

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

This theorem is referenced by:  eqid  2229  sb8ab  2351  cbvabw  2352  cbvab  2353  vjust  2801  nfccdeq  3027  csbcow  3136  difeqri  3325  uneqri  3347  incom  3397  ineqri  3398  difin  3442  invdif  3447  indif  3448  difundi  3457  indifdir  3461  rabsnif  3736  pwv  3890  uniun  3910  intun  3957  intpr  3958  iuncom  3974  iuncom4  3975  iun0  4025  0iun  4026  iunin2  4032  iunun  4047  iunxun  4048  iunxiun  4050  iinpw  4059  inuni  4243  unidif0  4255  unipw  4307  snnex  4543  unon  4607  xpiundi  4782  xpiundir  4783  0xp  4804  iunxpf  4876  cnvuni  4914  dmiun  4938  dmuni  4939  epini  5105  rniun  5145  cnvresima  5224  imaco  5240  rnco  5241  dfmpt3  5452  imaiun  5896  opabex3d  6278  opabex3  6279  ecid  6762  qsid  6764  mapval2  6842  ixpin  6887  dfz2  9542  infssuzex  10483  dfrp2  10513  1nprm  12676  infpn2  13067  rrgval  14266  2idlval  14506  cnfldui  14593  zrhval  14621  plyun0  15450  edgval  15901  clwwlkn0  16203  clwwlknonmpo  16223  clwwlknon  16224  clwwlk0on0  16226