Theorem eqriv 2758

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

Syntax hints:   ↔ wb 208   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  eqid  2761  cbvabv  2831  cbvabw  2832  cbvab  2833  vjust  3454  rabtru  3648  nfccdeq  3740  csbgfi  3872  difeqri  4082  uneqri  4109  ineqri  4164  symdifass  4214  indifdi  4246  undif3  4252  csbcom  4373  csbab  4393  pwpr  4858  pwtp  4859  pwv  4861  uniun  4887  int0  4919  intun  4937  iuncom  4956  iuncom4  4957  iunin2  5027  iinun2  5029  iundif2  5030  iunun  5049  iunxun  5050  iunxiun  5053  iinpw  5062  inuni  5305  unipw  5416  xpiundi  5716  xpiundir  5717  iunxpf  5818  cnvuni  5860  dmiun  5887  dmuni  5888  idinxpres  6033  rniun  6129  xpdifid  6150  cnvresima  6213  imaco  6234  rnco  6235  rncoOLD  6236  imaindm  6282  dfmpt3  6651  imaiun  7225  unon  7807  opabex3d  7942  opabex3rd  7943  opabex3  7944  fparlem1  8086  fparlem2  8087  oarec  8526  ecid  8757  qsid  8758  mapval2  8850  ixpin  8901  onfin2  9181  unfilem1  9245  unifpw  9295  dfom5  9602  alephsuc2  10033  ackbij2  10195  isf33lem  10320  dffin7-2  10352  fin1a2lem6  10359  acncc  10394  fin41  10398  iunfo  10493  grutsk  10777  grothac  10785  grothtsk  10790  dfz2  12584  qexALT  12962  dfrp2  13395  om2uzrani  13962  hashkf  14342  divalglem4  16413  1nprm  16696  nsgacs  19186  oppgsubm  19385  oppgsubg  19386  oppgcntz  19387  pmtrprfvalrn  19511  opprsubg  20380  opprunit  20405  opprirred  20450  opprsubrng  20588  opprsubrg  20622  00lss  20988  dfprm2  21505  unocv  21712  iunocv  21713  00ply1bas  22281  toprntopon  22965  unisngl  23567  zcld  24854  iundisj  25590  plyun0  26237  aannenlem2  26370  dfz12s2  28558  eqid1  30615  choc0  31475  chocnul  31477  spanunsni  31728  lncnbd  32187  adjbd1o  32234  rnbra  32256  pjimai  32325  iunin1f  32706  iundisjf  32738  xrdifh  32932  iundisjfi  32948  opprnsg  33633  0mplrim  33772  ccfldextdgrr  33930  cmpcref  34108  eulerpartgbij  34630  eulerpartlemr  34632  oddprm2  34913  dfdm5  36087  dfrn5  36088  dffix2  36217  fixcnv  36220  dfom5b  36224  fnimage  36241  brimg  36249  bj-csbsnlem  37352  bj-projun  37443  bj-pw0ALT  37498  bj-vjust  37504  finxp1o  37850  iundif1  38057  poimirlem26  38109  csbcom2fi  38591  dfsucmap3  38926  prtlem16  39457  sn-iotalem  42804  redvmptabs  42933  aaitgo  43703  imaiun1  44191  grumnueq  44827  nzss  44857  dfodd2  48222  dfeven5  48252  dfodd7  48253  ixpv  49475  isoval2  49620  oppcciceq  49637  oppczeroo  49822  dfinito4  50086  lmdfval2  50240  cmdfval2  50241  initocmd  50254  termolmd  50255