Theorem eqriv 2137

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 2134	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1430	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 104   = wceq 1332   ∈ wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  eqid  2140  sb8ab  2262  cbvabw  2263  cbvab  2264  vjust  2690  nfccdeq  2911  difeqri  3201  uneqri  3223  incom  3273  ineqri  3274  difin  3318  invdif  3323  indif  3324  difundi  3333  indifdir  3337  pwv  3743  uniun  3763  intun  3810  intpr  3811  iuncom  3827  iuncom4  3828  iun0  3877  0iun  3878  iunin2  3884  iunun  3899  iunxun  3900  iunxiun  3902  iinpw  3911  inuni  4088  unidif0  4099  unipw  4147  snnex  4377  unon  4435  xpiundi  4605  xpiundir  4606  0xp  4627  iunxpf  4695  cnvuni  4733  dmiun  4756  dmuni  4757  epini  4918  rniun  4957  cnvresima  5036  imaco  5052  rnco  5053  dfmpt3  5253  imaiun  5669  opabex3d  6027  opabex3  6028  ecid  6500  qsid  6502  mapval2  6580  ixpin  6625  dfz2  9147  infssuzex  11678  1nprm  11831