Theorem eqriv 2167

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

Syntax hints:   ↔ wb 104   = wceq 1348   ∈ wcel 2141

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 1442  ax-ext 2152

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

This theorem is referenced by:  eqid  2170  sb8ab  2292  cbvabw  2293  cbvab  2294  vjust  2731  nfccdeq  2953  csbcow  3060  difeqri  3247  uneqri  3269  incom  3319  ineqri  3320  difin  3364  invdif  3369  indif  3370  difundi  3379  indifdir  3383  pwv  3795  uniun  3815  intun  3862  intpr  3863  iuncom  3879  iuncom4  3880  iun0  3929  0iun  3930  iunin2  3936  iunun  3951  iunxun  3952  iunxiun  3954  iinpw  3963  inuni  4141  unidif0  4153  unipw  4202  snnex  4433  unon  4495  xpiundi  4669  xpiundir  4670  0xp  4691  iunxpf  4759  cnvuni  4797  dmiun  4820  dmuni  4821  epini  4982  rniun  5021  cnvresima  5100  imaco  5116  rnco  5117  dfmpt3  5320  imaiun  5739  opabex3d  6100  opabex3  6101  ecid  6576  qsid  6578  mapval2  6656  ixpin  6701  dfz2  9284  dfrp2  10220  infssuzex  11904  1nprm  12068  infpn2  12411