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 1502	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ 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 1498  ax-ext 2213

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

This theorem is referenced by:  eqid  2231  sb8ab  2354  cbvabw  2355  cbvab  2356  vjust  2804  nfccdeq  3030  csbcow  3139  difeqri  3329  uneqri  3351  incom  3401  ineqri  3402  difin  3446  invdif  3451  indif  3452  difundi  3461  indifdir  3465  rabsnif  3742  pwv  3897  uniun  3917  intun  3964  intpr  3965  iuncom  3981  iuncom4  3982  iun0  4032  0iun  4033  iunin2  4039  iunun  4054  iunxun  4055  iunxiun  4057  iinpw  4066  inuni  4250  unidif0  4263  unipw  4315  snnex  4551  unon  4615  xpiundi  4790  xpiundir  4791  0xp  4812  iunxpf  4884  cnvuni  4922  dmiun  4946  dmuni  4947  epini  5114  rniun  5154  cnvresima  5233  imaco  5249  rnco  5250  dfmpt3  5462  imaiun  5911  opabex3d  6292  opabex3  6293  ecid  6810  qsid  6812  mapval2  6890  ixpin  6935  dfz2  9595  infssuzex  10537  dfrp2  10567  1nprm  12747  infpn2  13138  rrgval  14338  2idlval  14578  cnfldui  14665  zrhval  14693  plyun0  15527  edgval  15981  clwwlkn0  16329  clwwlknonmpo  16349  clwwlknon  16350  clwwlk0on0  16352