Theorem eqriv 2818

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  eqid  2821  cbvabv  2889  cbvabw  2890  cbvab  2891  vjust  3495  rabtru  3677  nfccdeq  3769  csbgfi  3903  difeqri  4101  uneqri  4127  incomOLD  4179  ineqri  4180  symdifass  4228  indifdir  4260  undif3  4265  csbcom  4369  csbab  4389  pwpr  4832  pwtp  4833  pwv  4835  uniun  4861  int0  4890  intun  4908  intpr  4909  iuncom  4926  iuncom4  4927  iunin2  4993  iinun2  4995  iundif2  4996  iunun  5015  iunxun  5016  iunxiun  5019  iinpw  5028  inuni  5246  unipw  5343  xpiundi  5622  xpiundir  5623  iunxpf  5719  cnvuni  5757  dmiun  5782  dmuni  5783  idinxpres  5914  epini  5959  rniun  6006  xpdifid  6025  cnvresima  6087  imaco  6104  rnco  6105  dfmpt3  6482  imaiun  7004  unon  7546  opabex3d  7666  opabex3rd  7667  opabex3  7668  fparlem1  7807  fparlem2  7808  oarec  8188  ecid  8362  qsid  8363  mapval2  8436  ixpin  8487  onfin2  8710  unfilem1  8782  unifpw  8827  dfom5  9113  alephsuc2  9506  ackbij2  9665  isf33lem  9788  dffin7-2  9820  fin1a2lem6  9827  acncc  9862  fin41  9866  iunfo  9961  grutsk  10244  grothac  10252  grothtsk  10257  dfz2  12001  qexALT  12364  om2uzrani  13321  hashkf  13693  divalglem4  15747  1nprm  16023  nsgacs  18314  oppgsubm  18490  oppgsubg  18491  oppgcntz  18492  pmtrprfvalrn  18616  opprsubg  19386  opprunit  19411  opprirred  19452  opprsubrg  19556  00lss  19713  00ply1bas  20408  dfprm2  20641  unocv  20824  iunocv  20825  toprntopon  21533  unisngl  22135  zcld  23421  iundisj  24149  plyun0  24787  aannenlem2  24918  eqid1  28246  choc0  29103  chocnul  29105  spanunsni  29356  lncnbd  29815  adjbd1o  29862  rnbra  29884  pjimai  29953  iunin1f  30309  iundisjf  30339  dfrp2  30491  xrdifh  30503  iundisjfi  30519  ccfldextdgrr  31057  cmpcref  31114  eulerpartgbij  31630  eulerpartlemr  31632  oddprm2  31926  dfdm5  33016  dfrn5  33017  imaindm  33022  dffix2  33366  fixcnv  33369  dfom5b  33373  fnimage  33390  brimg  33398  bj-csbsnlem  34223  bj-projun  34309  bj-pw0ALT  34345  bj-vjust  34349  finxp1o  34676  wl-dfrabv  34877  iundif1  34881  poimirlem26  34933  csbcom2fi  35421  prtlem16  36020  aaitgo  39811  imaiun1  40045  grumnueq  40672  nzss  40698  dfodd2  43850  dfeven5  43880  dfodd7  43881