Theorem eqriv 2235

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

Syntax hints:   ↔ wb 105   = wceq 1402   ∈ wcel 2209

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 1502  ax-ext 2220

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

This theorem is referenced by:  eqid  2238  sb8ab  2362  cbvabw  2363  cbvab  2364  vjust  2822  nfccdeq  3049  csbcow  3158  difeqri  3349  uneqri  3371  incom  3421  ineqri  3424  difin  3468  invdif  3473  indif  3474  difundi  3483  indifdir  3487  rabsnif  3777  pwv  3932  uniun  3952  intun  3999  intpr  4000  iuncom  4016  iuncom4  4017  iun0  4067  0iun  4068  iunin2  4074  iunun  4089  iunxun  4090  iunxiun  4092  iinpw  4101  inuni  4289  unidif0  4302  unipw  4355  snnex  4592  unon  4656  xpiundi  4831  xpiundir  4832  0xp  4853  iunxpf  4926  cnvuni  4964  dmiun  4988  dmuni  4989  epini  5156  rniun  5196  cnvresima  5275  imaco  5291  rnco  5292  dfmpt3  5504  imaiun  5960  opabex3d  6344  opabex3  6345  ecid  6866  qsid  6868  mapval2  6953  ixpin  6999  dfz2  9700  infssuzex  10649  dfrp2  10681  1nprm  12875  infpn2  13330  mgpplusg  14205  mgpbas  14208  ringidval  14248  rrgval  14553  2idlval  14822  cnfldui  14907  zrhval  14935  asclfval  15004  plyun0  15820  edgval  16284  clwwlkn0  16632  clwwlknonmpo  16652  clwwlknon  16653  clwwlk0on0  16655