Theorem eqriv 2092

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

Syntax hints:   ↔ wb 104   = wceq 1296   ∈ wcel 1445

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

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

This theorem is referenced by:  eqid  2095  sb8ab  2216  cbvab  2217  vjust  2634  nfccdeq  2852  difeqri  3135  uneqri  3157  incom  3207  ineqri  3208  difin  3252  invdif  3257  indif  3258  difundi  3267  indifdir  3271  pwv  3674  uniun  3694  intun  3741  intpr  3742  iuncom  3758  iuncom4  3759  iun0  3808  0iun  3809  iunin2  3815  iunun  3830  iunxun  3831  iunxiun  3832  iinpw  3841  inuni  4012  unidif0  4023  unipw  4068  snnex  4298  unon  4356  xpiundi  4525  xpiundir  4526  0xp  4547  iunxpf  4615  cnvuni  4653  dmiun  4676  dmuni  4677  epini  4836  rniun  4875  cnvresima  4954  imaco  4970  rnco  4971  dfmpt3  5170  imaiun  5577  opabex3d  5930  opabex3  5931  ecid  6395  qsid  6397  mapval2  6475  ixpin  6520  dfz2  8917  infssuzex  11372  1nprm  11523