Theorem eqriv 2726

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqid  2729  cbvabv  2799  cbvabw  2800  cbvab  2801  vjust  3439  rabtru  3647  nfccdeq  3740  csbgfi  3873  difeqri  4081  uneqri  4109  ineqri  4165  symdifass  4215  indifdi  4247  undif3  4253  csbcom  4373  csbab  4393  pwpr  4855  pwtp  4856  pwv  4858  uniun  4884  int0  4915  intun  4933  iuncom  4952  iuncom4  4953  iunin2  5023  iinun2  5025  iundif2  5026  iunun  5045  iunxun  5046  iunxiun  5049  iinpw  5058  inuni  5292  unipw  5397  xpiundi  5694  xpiundir  5695  iunxpf  5795  cnvuni  5833  dmiun  5860  dmuni  5861  idinxpres  6002  rniun  6100  xpdifid  6121  cnvresima  6183  imaco  6204  rnco  6205  imaindm  6251  dfmpt3  6620  imaiun  7185  unon  7770  opabex3d  7907  opabex3rd  7908  opabex3  7909  fparlem1  8052  fparlem2  8053  oarec  8487  ecid  8714  qsid  8715  mapval2  8806  ixpin  8857  onfin2  9140  unfilem1  9212  unifpw  9264  dfom5  9565  alephsuc2  9993  ackbij2  10155  isf33lem  10279  dffin7-2  10311  fin1a2lem6  10318  acncc  10353  fin41  10357  iunfo  10452  grutsk  10735  grothac  10743  grothtsk  10748  dfz2  12508  qexALT  12883  dfrp2  13315  om2uzrani  13877  hashkf  14257  divalglem4  16325  1nprm  16608  nsgacs  19059  oppgsubm  19259  oppgsubg  19260  oppgcntz  19261  pmtrprfvalrn  19385  opprsubg  20255  opprunit  20280  opprirred  20325  opprsubrng  20462  opprsubrg  20496  00lss  20862  dfprm2  21398  unocv  21605  iunocv  21606  00ply1bas  22140  toprntopon  22828  unisngl  23430  zcld  24718  iundisj  25465  plyun0  26118  aannenlem2  26253  eqid1  30429  choc0  31288  chocnul  31290  spanunsni  31541  lncnbd  32000  adjbd1o  32047  rnbra  32069  pjimai  32138  iunin1f  32519  iundisjf  32551  xrdifh  32736  iundisjfi  32752  opprnsg  33431  ccfldextdgrr  33643  cmpcref  33816  eulerpartgbij  34339  eulerpartlemr  34341  oddprm2  34622  dfdm5  35745  dfrn5  35746  dffix2  35878  fixcnv  35881  dfom5b  35885  fnimage  35902  brimg  35910  bj-csbsnlem  36876  bj-projun  36967  bj-pw0ALT  37022  bj-vjust  37028  finxp1o  37365  iundif1  37573  poimirlem26  37625  csbcom2fi  38107  prtlem16  38847  sn-iotalem  42194  redvmptabs  42333  aaitgo  43135  imaiun1  43624  grumnueq  44260  nzss  44290  dfodd2  47621  dfeven5  47651  dfodd7  47652  ixpv  48875  isoval2  49021  oppcciceq  49038  oppczeroo  49223  dfinito4  49487  lmdfval2  49641  cmdfval2  49642  initocmd  49655  termolmd  49656