Theorem eqriv 2162

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

Syntax hints:   ↔ wb 104   = wceq 1343   ∈ wcel 2136

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 1437  ax-ext 2147

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

This theorem is referenced by:  eqid  2165  sb8ab  2288  cbvabw  2289  cbvab  2290  vjust  2727  nfccdeq  2949  csbcow  3056  difeqri  3242  uneqri  3264  incom  3314  ineqri  3315  difin  3359  invdif  3364  indif  3365  difundi  3374  indifdir  3378  pwv  3788  uniun  3808  intun  3855  intpr  3856  iuncom  3872  iuncom4  3873  iun0  3922  0iun  3923  iunin2  3929  iunun  3944  iunxun  3945  iunxiun  3947  iinpw  3956  inuni  4134  unidif0  4146  unipw  4195  snnex  4426  unon  4488  xpiundi  4662  xpiundir  4663  0xp  4684  iunxpf  4752  cnvuni  4790  dmiun  4813  dmuni  4814  epini  4975  rniun  5014  cnvresima  5093  imaco  5109  rnco  5110  dfmpt3  5310  imaiun  5728  opabex3d  6089  opabex3  6090  ecid  6564  qsid  6566  mapval2  6644  ixpin  6689  dfz2  9263  dfrp2  10199  infssuzex  11882  1nprm  12046  infpn2  12389