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  2738  nfccdeq  2960  csbcow  3068  difeqri  3255  uneqri  3277  incom  3327  ineqri  3328  difin  3372  invdif  3377  indif  3378  difundi  3387  indifdir  3391  pwv  3807  uniun  3827  intun  3874  intpr  3875  iuncom  3891  iuncom4  3892  iun0  3941  0iun  3942  iunin2  3948  iunun  3963  iunxun  3964  iunxiun  3966  iinpw  3975  inuni  4153  unidif0  4165  unipw  4215  snnex  4446  unon  4508  xpiundi  4682  xpiundir  4683  0xp  4704  iunxpf  4772  cnvuni  4810  dmiun  4833  dmuni  4834  epini  4996  rniun  5036  cnvresima  5115  imaco  5131  rnco  5132  dfmpt3  5335  imaiun  5756  opabex3d  6117  opabex3  6118  ecid  6593  qsid  6595  mapval2  6673  ixpin  6718  dfz2  9319  dfrp2  10257  infssuzex  11940  1nprm  12104  infpn2  12447