Theorem eqriv 2085

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

Syntax hints:   ↔ wb 103   = wceq 1289   ∈ wcel 1438

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081

This theorem is referenced by:  eqid  2088  sb8ab  2209  cbvab  2210  vjust  2620  nfccdeq  2836  difeqri  3118  uneqri  3140  incom  3190  ineqri  3191  difin  3234  invdif  3239  indif  3240  difundi  3249  indifdir  3253  pwv  3647  uniun  3667  intun  3714  intpr  3715  iuncom  3731  iuncom4  3732  iun0  3781  0iun  3782  iunin2  3788  iunun  3803  iunxun  3804  iunxiun  3805  iinpw  3811  inuni  3983  unidif0  3994  unipw  4035  snnex  4262  unon  4318  xpiundi  4484  xpiundir  4485  0xp  4506  iunxpf  4572  cnvuni  4610  dmiun  4633  dmuni  4634  epini  4790  rniun  4829  cnvresima  4907  imaco  4923  rnco  4924  dfmpt3  5122  imaiun  5521  opabex3d  5874  opabex3  5875  ecid  6335  qsid  6337  mapval2  6415  dfz2  8789  infssuzex  11038  1nprm  11189