Theorem eqriv 2737

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

Syntax hints:   ↔ wb 207   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  eqid  2740  cbvabv  2810  cbvabw  2811  cbvab  2812  vjust  3433  rabtru  3634  nfccdeq  3726  csbgfi  3858  difeqri  4066  uneqri  4093  ineqri  4148  symdifass  4197  indifdi  4229  undif3  4235  csbcom  4355  csbab  4375  pwpr  4839  pwtp  4840  pwv  4842  uniun  4868  int0  4899  intun  4917  iuncom  4936  iuncom4  4937  iunin2  5007  iinun2  5009  iundif2  5010  iunun  5029  iunxun  5030  iunxiun  5033  iinpw  5042  inuni  5285  unipw  5396  xpiundi  5696  xpiundir  5697  iunxpf  5797  cnvuni  5835  dmiun  5862  dmuni  5863  idinxpres  6006  rniun  6105  xpdifid  6126  cnvresima  6188  imaco  6209  rnco  6210  rncoOLD  6211  imaindm  6257  dfmpt3  6626  imaiun  7196  unon  7778  opabex3d  7914  opabex3rd  7915  opabex3  7916  fparlem1  8058  fparlem2  8059  oarec  8494  ecid  8724  qsid  8725  mapval2  8817  ixpin  8868  onfin2  9148  unfilem1  9212  unifpw  9262  dfom5  9569  alephsuc2  10000  ackbij2  10162  isf33lem  10286  dffin7-2  10318  fin1a2lem6  10325  acncc  10360  fin41  10364  iunfo  10459  grutsk  10743  grothac  10751  grothtsk  10756  dfz2  12541  qexALT  12912  dfrp2  13345  om2uzrani  13912  hashkf  14292  divalglem4  16363  1nprm  16646  nsgacs  19135  oppgsubm  19335  oppgsubg  19336  oppgcntz  19337  pmtrprfvalrn  19461  opprsubg  20330  opprunit  20355  opprirred  20400  opprsubrng  20538  opprsubrg  20572  00lss  20938  dfprm2  21455  unocv  21662  iunocv  21663  00ply1bas  22231  toprntopon  22915  unisngl  23517  zcld  24804  iundisj  25540  plyun0  26187  aannenlem2  26320  dfz12s2  28505  eqid1  30562  choc0  31422  chocnul  31424  spanunsni  31675  lncnbd  32134  adjbd1o  32181  rnbra  32203  pjimai  32272  iunin1f  32653  iundisjf  32685  xrdifh  32879  iundisjfi  32895  opprnsg  33574  0mplrim  33705  ccfldextdgrr  33863  cmpcref  34041  eulerpartgbij  34563  eulerpartlemr  34565  oddprm2  34846  dfdm5  36008  dfrn5  36009  dffix2  36138  fixcnv  36141  dfom5b  36145  fnimage  36162  brimg  36170  bj-csbsnlem  37263  bj-projun  37354  bj-pw0ALT  37409  bj-vjust  37415  finxp1o  37761  iundif1  37968  poimirlem26  38020  csbcom2fi  38502  dfsucmap3  38837  prtlem16  39368  sn-iotalem  42715  redvmptabs  42844  aaitgo  43614  imaiun1  44102  grumnueq  44738  nzss  44768  dfodd2  48134  dfeven5  48164  dfodd7  48165  ixpv  49387  isoval2  49532  oppcciceq  49549  oppczeroo  49734  dfinito4  49998  lmdfval2  50152  cmdfval2  50153  initocmd  50166  termolmd  50167