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  3679  nfccdeq  3773  csbgfi  3913  difeqri  4123  uneqri  4150  ineqri  4203  symdifass  4250  indifdi  4282  indifdirOLD  4284  undif3  4289  csbcom  4416  csbab  4436  pwpr  4901  pwtp  4902  pwv  4904  uniun  4933  int0  4965  intun  4983  intprOLD  4986  iuncom  5003  iuncom4  5004  iunin2  5073  iinun2  5075  iundif2  5076  iunun  5095  iunxun  5096  iunxiun  5099  iinpw  5108  inuni  5342  unipw  5449  xpiundi  5744  xpiundir  5745  iunxpf  5846  cnvuni  5884  dmiun  5911  dmuni  5912  idinxpres  6044  rniun  6144  xpdifid  6164  cnvresima  6226  imaco  6247  rnco  6248  imaindm  6295  dfmpt3  6681  imaiun  7239  unon  7814  opabex3d  7947  opabex3rd  7948  opabex3  7949  fparlem1  8093  fparlem2  8094  oarec  8558  ecid  8772  qsid  8773  mapval2  8862  ixpin  8913  onfin2  9227  unfilem1  9306  unifpw  9351  dfom5  9641  alephsuc2  10071  ackbij2  10234  isf33lem  10357  dffin7-2  10389  fin1a2lem6  10396  acncc  10431  fin41  10435  iunfo  10530  grutsk  10813  grothac  10821  grothtsk  10826  dfz2  12573  qexALT  12944  dfrp2  13369  om2uzrani  13913  hashkf  14288  divalglem4  16335  1nprm  16612  nsgacs  19036  oppgsubm  19222  oppgsubg  19223  oppgcntz  19224  pmtrprfvalrn  19349  opprsubg  20155  opprunit  20180  opprirred  20225  opprsubrg  20372  00lss  20540  dfprm2  21027  unocv  21217  iunocv  21218  00ply1bas  21744  toprntopon  22409  unisngl  23013  zcld  24311  iundisj  25047  plyun0  25693  aannenlem2  25824  eqid1  29700  choc0  30557  chocnul  30559  spanunsni  30810  lncnbd  31269  adjbd1o  31316  rnbra  31338  pjimai  31407  iunin1f  31767  iundisjf  31798  xrdifh  31969  iundisjfi  31985  opprnsg  32551  ccfldextdgrr  32691  cmpcref  32768  eulerpartgbij  33309  eulerpartlemr  33311  oddprm2  33605  dfdm5  34682  dfrn5  34683  dffix2  34815  fixcnv  34818  dfom5b  34822  fnimage  34839  brimg  34847  bj-csbsnlem  35721  bj-projun  35813  bj-pw0ALT  35868  bj-vjust  35874  finxp1o  36211  iundif1  36400  poimirlem26  36452  csbcom2fi  36934  prtlem16  37677  sn-iotalem  40986  aaitgo  41837  imaiun1  42335  grumnueq  42979  nzss  43009  dfodd2  46239  dfeven5  46269  dfodd7  46270  opprsubrng  46671