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  3808  uniun  3828  intun  3875  intpr  3876  iuncom  3892  iuncom4  3893  iun0  3943  0iun  3944  iunin2  3950  iunun  3965  iunxun  3966  iunxiun  3968  iinpw  3977  inuni  4155  unidif0  4167  unipw  4217  snnex  4448  unon  4510  xpiundi  4684  xpiundir  4685  0xp  4706  iunxpf  4775  cnvuni  4813  dmiun  4836  dmuni  4837  epini  4999  rniun  5039  cnvresima  5118  imaco  5134  rnco  5135  dfmpt3  5338  imaiun  5760  opabex3d  6121  opabex3  6122  ecid  6597  qsid  6599  mapval2  6677  ixpin  6722  dfz2  9324  dfrp2  10263  infssuzex  11949  1nprm  12113  infpn2  12456