Theorem eqriv 2193

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

Syntax hints:   ↔ wb 105   = wceq 1364   ∈ wcel 2167

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 1463  ax-ext 2178

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

This theorem is referenced by:  eqid  2196  sb8ab  2318  cbvabw  2319  cbvab  2320  vjust  2764  nfccdeq  2987  csbcow  3095  difeqri  3284  uneqri  3306  incom  3356  ineqri  3357  difin  3401  invdif  3406  indif  3407  difundi  3416  indifdir  3420  pwv  3839  uniun  3859  intun  3906  intpr  3907  iuncom  3923  iuncom4  3924  iun0  3974  0iun  3975  iunin2  3981  iunun  3996  iunxun  3997  iunxiun  3999  iinpw  4008  inuni  4189  unidif0  4201  unipw  4251  snnex  4484  unon  4548  xpiundi  4722  xpiundir  4723  0xp  4744  iunxpf  4815  cnvuni  4853  dmiun  4876  dmuni  4877  epini  5041  rniun  5081  cnvresima  5160  imaco  5176  rnco  5177  dfmpt3  5383  imaiun  5810  opabex3d  6187  opabex3  6188  ecid  6666  qsid  6668  mapval2  6746  ixpin  6791  dfz2  9415  infssuzex  10340  dfrp2  10370  1nprm  12307  infpn2  12698  rrgval  13894  2idlval  14134  cnfldui  14221  zrhval  14249  plyun0  15056