Theorem eqriv 2204

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 2201	. 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 1477	1 |- A = B

Syntax hints:   <-> wb 105   = wceq 1373   e. wcel 2178

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 1473  ax-ext 2189

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

This theorem is referenced by:  eqid  2207  sb8ab  2329  cbvabw  2330  cbvab  2331  vjust  2777  nfccdeq  3003  csbcow  3112  difeqri  3301  uneqri  3323  incom  3373  ineqri  3374  difin  3418  invdif  3423  indif  3424  difundi  3433  indifdir  3437  pwv  3863  uniun  3883  intun  3930  intpr  3931  iuncom  3947  iuncom4  3948  iun0  3998  0iun  3999  iunin2  4005  iunun  4020  iunxun  4021  iunxiun  4023  iinpw  4032  inuni  4215  unidif0  4227  unipw  4279  snnex  4513  unon  4577  xpiundi  4751  xpiundir  4752  0xp  4773  iunxpf  4844  cnvuni  4882  dmiun  4906  dmuni  4907  epini  5072  rniun  5112  cnvresima  5191  imaco  5207  rnco  5208  dfmpt3  5418  imaiun  5852  opabex3d  6229  opabex3  6230  ecid  6708  qsid  6710  mapval2  6788  ixpin  6833  dfz2  9480  infssuzex  10413  dfrp2  10443  1nprm  12551  infpn2  12942  rrgval  14139  2idlval  14379  cnfldui  14466  zrhval  14494  plyun0  15323