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  2471  vjust  2860  nincom  3226  dblcompl  3227  difeqri  3387  uneqri  3406  incom  3448  ineqri  3449  indifdir  3511  undif3  3515  complab  3524  pwpr  3883  pwtp  3884  pwv  3886  unipr  3905  uniun  3910  intun  3958  intpr  3959  iuncom  3975  iuncom4  3976  iun0  4022  0iun  4023  iunin2  4030  iinun2  4032  iundif2  4033  iunun  4046  iunxun  4047  iunxiun  4048  iinuni  4049  iinpw  4054  unipw  4117  pwadjoin  4119  pw1un  4163  pw1in  4164  pw1sn  4165  df1c2  4168  imacok  4282  dfuni12  4291  dfimak2  4298  dfpw12  4301  dfuni3  4315  dfint3  4318  unipw1  4325  dfpw2  4327  addcid1  4405  addcass  4415  dfphi2  4569  proj1op  4600  proj2op  4601  setconslem4  4734  dfswap2  4741  xpiundi  4817  xpiundir  4818  iunxpf  4829  xp0r  4842  cnvuni  4895  dfrn4  4904  dmuni  4914  dfima3  4951  rnuni  5038  dmsnopg  5066  rnsnop  5075  cnvresima  5077  imaco  5086  rnco  5087  dfxp2  5113  imaiun  5464  dfdm4  5507  dfrn5  5508  dmsi  5519  dmtxp  5802  clos1baseima  5883  qsid  5990  mapval2  6018