Theorem eqriv 2762

Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
eqriv.1	⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)

Assertion

Ref	Expression
eqriv	⊢ 𝐴 = 𝐵

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eqriv

Step	Hyp	Ref	Expression
1		dfcleq 2758	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1822	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 209   = wceq 1563   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by:  eqid  2765  cbvabv  2835  cbvabw  2836  cbvab  2837  vjust  3458  rabtru  3651  nfccdeq  3744  csbgfi  3875  difeqri  4085  uneqri  4112  ineqri  4167  symdifass  4217  indifdi  4249  undif3  4255  csbcom  4377  csbab  4397  pwpr  4861  pwtp  4862  pwv  4864  uniun  4890  int0  4922  intun  4940  iuncom  4959  iuncom4  4960  iunin2  5030  iinun2  5032  iundif2  5033  iunun  5054  iunxun  5055  iunxiun  5058  iinpw  5067  inuni  5310  unipw  5421  xpiundi  5722  xpiundir  5723  iunxpf  5824  cnvuni  5866  dmiun  5893  dmuni  5894  idinxpres  6039  rniun  6135  xpdifid  6156  xpdifcnvepel  6157  cnvresima  6220  imaco  6241  rnco  6242  rncoOLD  6243  imaindm  6289  dfmpt3  6659  imaiun  7233  unon  7815  opabex3d  7950  opabex3rd  7951  opabex3  7952  fparlem1  8095  fparlem2  8096  oarec  8535  ecid  8766  qsid  8767  mapval2  8858  ixpin  8909  onfin2  9189  unfilem1  9253  unifpw  9300  dfom5  9607  alephsuc2  10052  ackbij2  10213  isf33lem  10338  dffin7-2  10370  fin1a2lem6  10377  acncc  10412  fin41  10416  iunfo  10511  grutsk  10795  grothac  10803  grothtsk  10808  dfz2  12598  qexALT  12976  dfrp2  13409  om2uzrani  13976  hashkf  14356  divalglem4  16442  1nprm  16725  nsgacs  19216  oppgsubm  19420  oppgsubg  19421  oppgcntz  19422  pmtrprfvalrn  19546  opprsubg  20422  opprunit  20447  opprirred  20492  opprsubrng  20632  opprsubrg  20666  00lss  21028  dfprm2  21580  unocv  21787  iunocv  21788  00ply1bas  22356  toprntopon  23039  unisngl  23641  zcld  24928  iundisj  25664  plyun0  26311  aannenlem2  26447  dfz12s2  28635  eqid1  30723  choc0  31583  chocnul  31585  spanunsni  31836  lncnbd  32295  adjbd1o  32342  rnbra  32364  pjimai  32433  iunin1f  32808  iundisjf  32840  xrdifh  33033  iundisjfi  33049  opprnsg  33678  0mplrim  33816  ccfldextdgrr  33974  cmpcref  34152  eulerpartgbij  34674  eulerpartlemr  34676  oddprm2  34954  dfdm5  36131  dfrn5  36132  dffix2  36261  fixcnv  36264  dfom5b  36268  fnimage  36285  brimg  36293  bj-csbsnlem  37395  bj-projun  37486  bj-pw0ALT  37541  bj-vjust  37547  finxp1o  37893  iundif1  38100  poimirlem26  38152  csbcom2fi  38634  dfsucmap3  38969  prtlem16  39500  sn-iotalem  42847  redvmptabs  42976  aaitgo  43746  imaiun1  44234  grumnueq  44856  nzss  44886  dfodd2  48257  dfeven5  48287  dfodd7  48288  dfidom2  48964  ixpv  49520  isoval2  49665  oppcciceq  49682  oppczeroo  49867  dfinito4  50131  lmdfval2  50285  cmdfval2  50286  initocmd  50299  termolmd  50300