Theorem eqriv 2350

Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqriv.1	⊢ (x ∈ A ↔ x ∈ B)

Assertion

Ref	Expression
eqriv	⊢ A = B

Distinct variable groups:   x,A   x,B

Proof of Theorem eqriv

Step	Hyp	Ref	Expression
1		dfcleq 2347	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
2		eqriv.1	. 2 ⊢ (x ∈ A ↔ x ∈ B)
3	1, 2	mpgbir 1550	1 ⊢ A = B

Syntax hints:   ↔ wb 176   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-cleq 2346

This theorem is referenced by:  eqid  2353  cbvab  2472  vjust  2861  nincom  3227  dblcompl  3228  difeqri  3388  uneqri  3407  incom  3449  ineqri  3450  indifdir  3512  undif3  3516  complab  3525  pwpr  3884  pwtp  3885  pwv  3887  unipr  3906  uniun  3911  intun  3959  intpr  3960  iuncom  3976  iuncom4  3977  iun0  4023  0iun  4024  iunin2  4031  iinun2  4033  iundif2  4034  iunun  4047  iunxun  4048  iunxiun  4049  iinuni  4050  iinpw  4055  unipw  4118  pwadjoin  4120  pw1un  4164  pw1in  4165  pw1sn  4166  df1c2  4169  imacok  4283  dfuni12  4292  dfimak2  4299  dfpw12  4302  dfuni3  4316  dfint3  4319  unipw1  4326  dfpw2  4328  addcid1  4406  addcass  4416  dfphi2  4570  proj1op  4601  proj2op  4602  setconslem4  4735  dfswap2  4742  xpiundi  4818  xpiundir  4819  iunxpf  4830  xp0r  4843  cnvuni  4896  dfrn4  4905  dmuni  4915  dfima3  4952  rnuni  5039  dmsnopg  5067  rnsnop  5076  cnvresima  5078  imaco  5087  rnco  5088  dfxp2  5114  imaiun  5465  dfdm4  5508  dfrn5  5509  dmsi  5520  dmtxp  5803  clos1baseima  5884  qsid  5991  mapval2  6019