Theorem eqriv 2226

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

Syntax hints:   ↔ wb 105   = wceq 1395   ∈ wcel 2200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  eqid  2229  sb8ab  2351  cbvabw  2352  cbvab  2353  vjust  2800  nfccdeq  3026  csbcow  3135  difeqri  3324  uneqri  3346  incom  3396  ineqri  3397  difin  3441  invdif  3446  indif  3447  difundi  3456  indifdir  3460  pwv  3886  uniun  3906  intun  3953  intpr  3954  iuncom  3970  iuncom4  3971  iun0  4021  0iun  4022  iunin2  4028  iunun  4043  iunxun  4044  iunxiun  4046  iinpw  4055  inuni  4238  unidif0  4250  unipw  4302  snnex  4536  unon  4600  xpiundi  4774  xpiundir  4775  0xp  4796  iunxpf  4867  cnvuni  4905  dmiun  4929  dmuni  4930  epini  5095  rniun  5135  cnvresima  5214  imaco  5230  rnco  5231  dfmpt3  5442  imaiun  5877  opabex3d  6256  opabex3  6257  ecid  6735  qsid  6737  mapval2  6815  ixpin  6860  dfz2  9507  infssuzex  10440  dfrp2  10470  1nprm  12622  infpn2  13013  rrgval  14211  2idlval  14451  cnfldui  14538  zrhval  14566  plyun0  15395