Theorem eqriv 2228

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 2225	. 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 1501	1 |- A = B

Syntax hints:   <-> wb 105   = wceq 1397   e. wcel 2202

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 1497  ax-ext 2213

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

This theorem is referenced by:  eqid  2231  sb8ab  2353  cbvabw  2354  cbvab  2355  vjust  2803  nfccdeq  3029  csbcow  3138  difeqri  3327  uneqri  3349  incom  3399  ineqri  3400  difin  3444  invdif  3449  indif  3450  difundi  3459  indifdir  3463  rabsnif  3738  pwv  3892  uniun  3912  intun  3959  intpr  3960  iuncom  3976  iuncom4  3977  iun0  4027  0iun  4028  iunin2  4034  iunun  4049  iunxun  4050  iunxiun  4052  iinpw  4061  inuni  4245  unidif0  4257  unipw  4309  snnex  4545  unon  4609  xpiundi  4784  xpiundir  4785  0xp  4806  iunxpf  4878  cnvuni  4916  dmiun  4940  dmuni  4941  epini  5107  rniun  5147  cnvresima  5226  imaco  5242  rnco  5243  dfmpt3  5455  imaiun  5900  opabex3d  6282  opabex3  6283  ecid  6766  qsid  6768  mapval2  6846  ixpin  6891  dfz2  9551  infssuzex  10492  dfrp2  10522  1nprm  12685  infpn2  13076  rrgval  14275  2idlval  14515  cnfldui  14602  zrhval  14630  plyun0  15459  edgval  15910  clwwlkn0  16258  clwwlknonmpo  16278  clwwlknon  16279  clwwlk0on0  16281