Theorem cleqri 1101

Description: Infer equality of sets from equivalence of membership.

Hypothesis

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

Assertion

Ref	Expression
cleqri	⊢ A = B

Distinct variable group(s):   x,A   x,B

Proof of Theorem cleqri

Step	Hyp	Ref	Expression
1		dfcleq 1098	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
2		cleqri.1	. 2 ⊢ (x ∈ A ↔ x ∈ B)
3	1, 2	mpgbir 686	1 ⊢ A = B

Syntax hints:   ↔ wb 127   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  cleqid 1102  uneqri 1602  uncom 1604  incom 1636  ineqri 1637  dfss4 1667  dfun2 1668  dfin2 1669  difin 1670  indi 1676  undi 1677  unab 1691  inab 1692  pwv 1884  uniun 1934  intun 1989  intpr 1990  iun0 2028  iunin2 2030  iinun2 2031  iundif2 2032  iunxsn 2034  iunxun 2035  iinuni 2036  iinpw 2038  unon 2338  xp0r 2474  cnvuni 2521  dmun 2536  dmuni 2538  rnuni 2646  imaiun 2650  dmco2 2673  erdmrn 3213  jech9.3 3510  om2uzran 4655  qnnen 4931  choc0 5291  chocnul 5293  spanunsn 5482

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-gen 677  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-cleq 1097

metamath.org