Theorem eqriv 2203

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

Syntax hints:   ↔ wb 105   = wceq 1373   ∈ wcel 2177

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 1473  ax-ext 2188

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

This theorem is referenced by:  eqid  2206  sb8ab  2328  cbvabw  2329  cbvab  2330  vjust  2774  nfccdeq  2998  csbcow  3106  difeqri  3295  uneqri  3317  incom  3367  ineqri  3368  difin  3412  invdif  3417  indif  3418  difundi  3427  indifdir  3431  pwv  3852  uniun  3872  intun  3919  intpr  3920  iuncom  3936  iuncom4  3937  iun0  3987  0iun  3988  iunin2  3994  iunun  4009  iunxun  4010  iunxiun  4012  iinpw  4021  inuni  4204  unidif0  4216  unipw  4266  snnex  4500  unon  4564  xpiundi  4738  xpiundir  4739  0xp  4760  iunxpf  4831  cnvuni  4869  dmiun  4893  dmuni  4894  epini  5059  rniun  5099  cnvresima  5178  imaco  5194  rnco  5195  dfmpt3  5405  imaiun  5839  opabex3d  6216  opabex3  6217  ecid  6695  qsid  6697  mapval2  6775  ixpin  6820  dfz2  9458  infssuzex  10389  dfrp2  10419  1nprm  12486  infpn2  12877  rrgval  14074  2idlval  14314  cnfldui  14401  zrhval  14429  plyun0  15258