Theorem eqriv 2190

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

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

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 1460  ax-ext 2175

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

This theorem is referenced by:  eqid  2193  sb8ab  2315  cbvabw  2316  cbvab  2317  vjust  2761  nfccdeq  2983  csbcow  3091  difeqri  3279  uneqri  3301  incom  3351  ineqri  3352  difin  3396  invdif  3401  indif  3402  difundi  3411  indifdir  3415  pwv  3834  uniun  3854  intun  3901  intpr  3902  iuncom  3918  iuncom4  3919  iun0  3969  0iun  3970  iunin2  3976  iunun  3991  iunxun  3992  iunxiun  3994  iinpw  4003  inuni  4184  unidif0  4196  unipw  4246  snnex  4479  unon  4543  xpiundi  4717  xpiundir  4718  0xp  4739  iunxpf  4810  cnvuni  4848  dmiun  4871  dmuni  4872  epini  5036  rniun  5076  cnvresima  5155  imaco  5171  rnco  5172  dfmpt3  5376  imaiun  5803  opabex3d  6173  opabex3  6174  ecid  6652  qsid  6654  mapval2  6732  ixpin  6777  dfz2  9389  dfrp2  10332  infssuzex  12086  1nprm  12252  infpn2  12613  rrgval  13758  2idlval  13998  cnfldui  14077  zrhval  14105  plyun0  14882