Theorem eqriv 2228

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

Syntax hints:   ↔ wb 105   = wceq 1397   ∈ wcel 2202

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 1497  ax-ext 2213

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

This theorem is referenced by:  eqid  2231  sb8ab  2353  cbvabw  2354  cbvab  2355  vjust  2803  nfccdeq  3029  csbcow  3138  difeqri  3327  uneqri  3349  incom  3399  ineqri  3400  difin  3444  invdif  3449  indif  3450  difundi  3459  indifdir  3463  rabsnif  3738  pwv  3892  uniun  3912  intun  3959  intpr  3960  iuncom  3976  iuncom4  3977  iun0  4027  0iun  4028  iunin2  4034  iunun  4049  iunxun  4050  iunxiun  4052  iinpw  4061  inuni  4245  unidif0  4257  unipw  4309  snnex  4545  unon  4609  xpiundi  4784  xpiundir  4785  0xp  4806  iunxpf  4878  cnvuni  4916  dmiun  4940  dmuni  4941  epini  5107  rniun  5147  cnvresima  5226  imaco  5242  rnco  5243  dfmpt3  5455  imaiun  5901  opabex3d  6283  opabex3  6284  ecid  6767  qsid  6769  mapval2  6847  ixpin  6892  dfz2  9552  infssuzex  10494  dfrp2  10524  1nprm  12691  infpn2  13082  rrgval  14282  2idlval  14522  cnfldui  14609  zrhval  14637  plyun0  15466  edgval  15917  clwwlkn0  16265  clwwlknonmpo  16285  clwwlknon  16286  clwwlk0on0  16288