Theorem eqriv 2190

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

Syntax hints:   ↔ wb 105   = wceq 1364   ∈ wcel 2164

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 1460  ax-ext 2175

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

This theorem is referenced by:  eqid  2193  sb8ab  2315  cbvabw  2316  cbvab  2317  vjust  2761  nfccdeq  2984  csbcow  3092  difeqri  3280  uneqri  3302  incom  3352  ineqri  3353  difin  3397  invdif  3402  indif  3403  difundi  3412  indifdir  3416  pwv  3835  uniun  3855  intun  3902  intpr  3903  iuncom  3919  iuncom4  3920  iun0  3970  0iun  3971  iunin2  3977  iunun  3992  iunxun  3993  iunxiun  3995  iinpw  4004  inuni  4185  unidif0  4197  unipw  4247  snnex  4480  unon  4544  xpiundi  4718  xpiundir  4719  0xp  4740  iunxpf  4811  cnvuni  4849  dmiun  4872  dmuni  4873  epini  5037  rniun  5077  cnvresima  5156  imaco  5172  rnco  5173  dfmpt3  5377  imaiun  5804  opabex3d  6175  opabex3  6176  ecid  6654  qsid  6656  mapval2  6734  ixpin  6779  dfz2  9392  dfrp2  10335  infssuzex  12089  1nprm  12255  infpn2  12616  rrgval  13761  2idlval  14001  cnfldui  14088  zrhval  14116  plyun0  14915