Theorem eqriv 2229

Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqriv.1	⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)

Assertion

Ref	Expression
eqriv	⊢ 𝐴 = 𝐵

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eqriv

Step	Hyp	Ref	Expression
1		dfcleq 2226	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1502	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ wcel 2203

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 1498  ax-ext 2214

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

This theorem is referenced by:  eqid  2232  sb8ab  2356  cbvabw  2357  cbvab  2358  vjust  2813  nfccdeq  3039  csbcow  3148  difeqri  3338  uneqri  3360  incom  3410  ineqri  3413  difin  3457  invdif  3462  indif  3463  difundi  3472  indifdir  3476  rabsnif  3757  pwv  3912  uniun  3932  intun  3979  intpr  3980  iuncom  3996  iuncom4  3997  iun0  4047  0iun  4048  iunin2  4054  iunun  4069  iunxun  4070  iunxiun  4072  iinpw  4081  inuni  4266  unidif0  4279  unipw  4332  snnex  4568  unon  4632  xpiundi  4807  xpiundir  4808  0xp  4829  iunxpf  4902  cnvuni  4940  dmiun  4964  dmuni  4965  epini  5132  rniun  5172  cnvresima  5251  imaco  5267  rnco  5268  dfmpt3  5480  imaiun  5932  opabex3d  6313  opabex3  6314  ecid  6831  qsid  6833  mapval2  6911  ixpin  6957  dfz2  9649  infssuzex  10592  dfrp2  10622  1nprm  12807  infpn2  13199  rrgval  14399  2idlval  14642  cnfldui  14729  zrhval  14757  plyun0  15593  edgval  16047  clwwlkn0  16395  clwwlknonmpo  16415  clwwlknon  16416  clwwlk0on0  16418