Theorem eqriv 2231

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

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ wcel 2205

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 1498  ax-ext 2216

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

This theorem is referenced by:  eqid  2234  sb8ab  2358  cbvabw  2359  cbvab  2360  vjust  2816  nfccdeq  3043  csbcow  3152  difeqri  3343  uneqri  3365  incom  3415  ineqri  3418  difin  3462  invdif  3467  indif  3468  difundi  3477  indifdir  3481  rabsnif  3763  pwv  3918  uniun  3938  intun  3985  intpr  3986  iuncom  4002  iuncom4  4003  iun0  4053  0iun  4054  iunin2  4060  iunun  4075  iunxun  4076  iunxiun  4078  iinpw  4087  inuni  4272  unidif0  4285  unipw  4338  snnex  4574  unon  4638  xpiundi  4813  xpiundir  4814  0xp  4835  iunxpf  4908  cnvuni  4946  dmiun  4970  dmuni  4971  epini  5138  rniun  5178  cnvresima  5257  imaco  5273  rnco  5274  dfmpt3  5486  imaiun  5939  opabex3d  6323  opabex3  6324  ecid  6845  qsid  6847  mapval2  6925  ixpin  6971  dfz2  9667  infssuzex  10615  dfrp2  10647  1nprm  12836  infpn2  13291  rrgval  14493  2idlval  14762  cnfldui  14849  zrhval  14877  plyun0  15713  edgval  16167  clwwlkn0  16515  clwwlknonmpo  16535  clwwlknon  16536  clwwlk0on0  16538