Theorem eqriv 2730

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqid  2733  cbvabv  2806  cbvabw  2807  cbvabwOLD  2808  cbvab  2809  vjust  3476  rabtru  3681  nfccdeq  3775  csbgfi  3915  difeqri  4125  uneqri  4152  ineqri  4205  symdifass  4252  indifdi  4284  indifdirOLD  4286  undif3  4291  csbcom  4418  csbab  4438  pwpr  4903  pwtp  4904  pwv  4906  uniun  4935  int0  4967  intun  4985  intprOLD  4988  iuncom  5005  iuncom4  5006  iunin2  5075  iinun2  5077  iundif2  5078  iunun  5097  iunxun  5098  iunxiun  5101  iinpw  5110  inuni  5344  unipw  5451  xpiundi  5747  xpiundir  5748  iunxpf  5849  cnvuni  5887  dmiun  5914  dmuni  5915  idinxpres  6047  rniun  6148  xpdifid  6168  cnvresima  6230  imaco  6251  rnco  6252  imaindm  6299  dfmpt3  6685  imaiun  7244  unon  7819  opabex3d  7952  opabex3rd  7953  opabex3  7954  fparlem1  8098  fparlem2  8099  oarec  8562  ecid  8776  qsid  8777  mapval2  8866  ixpin  8917  onfin2  9231  unfilem1  9310  unifpw  9355  dfom5  9645  alephsuc2  10075  ackbij2  10238  isf33lem  10361  dffin7-2  10393  fin1a2lem6  10400  acncc  10435  fin41  10439  iunfo  10534  grutsk  10817  grothac  10825  grothtsk  10830  dfz2  12577  qexALT  12948  dfrp2  13373  om2uzrani  13917  hashkf  14292  divalglem4  16339  1nprm  16616  nsgacs  19042  oppgsubm  19229  oppgsubg  19230  oppgcntz  19231  pmtrprfvalrn  19356  opprsubg  20166  opprunit  20191  opprirred  20236  opprsubrg  20340  00lss  20552  dfprm2  21043  unocv  21233  iunocv  21234  00ply1bas  21762  toprntopon  22427  unisngl  23031  zcld  24329  iundisj  25065  plyun0  25711  aannenlem2  25842  eqid1  29720  choc0  30579  chocnul  30581  spanunsni  30832  lncnbd  31291  adjbd1o  31338  rnbra  31360  pjimai  31429  iunin1f  31789  iundisjf  31820  xrdifh  31991  iundisjfi  32007  opprnsg  32598  ccfldextdgrr  32746  cmpcref  32830  eulerpartgbij  33371  eulerpartlemr  33373  oddprm2  33667  dfdm5  34744  dfrn5  34745  dffix2  34877  fixcnv  34880  dfom5b  34884  fnimage  34901  brimg  34909  bj-csbsnlem  35783  bj-projun  35875  bj-pw0ALT  35930  bj-vjust  35936  finxp1o  36273  iundif1  36462  poimirlem26  36514  csbcom2fi  36996  prtlem16  37739  sn-iotalem  41038  aaitgo  41904  imaiun1  42402  grumnueq  43046  nzss  43076  dfodd2  46304  dfeven5  46334  dfodd7  46335  opprsubrng  46738