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 1797	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqid  2740  cbvabv  2815  cbvabw  2816  cbvab  2817  vjust  3489  rabtru  3705  nfccdeq  3800  csbgfi  3942  difeqri  4151  uneqri  4179  ineqri  4233  symdifass  4281  indifdi  4313  undif3  4319  csbcom  4443  csbab  4463  pwpr  4925  pwtp  4926  pwv  4928  uniun  4954  int0  4986  intun  5004  iuncom  5022  iuncom4  5023  iunin2  5094  iinun2  5096  iundif2  5097  iunun  5116  iunxun  5117  iunxiun  5120  iinpw  5129  inuni  5368  unipw  5470  xpiundi  5770  xpiundir  5771  iunxpf  5873  cnvuni  5911  dmiun  5938  dmuni  5939  idinxpres  6076  rniun  6179  xpdifid  6199  cnvresima  6261  imaco  6282  rnco  6283  imaindm  6330  dfmpt3  6714  imaiun  7282  unon  7867  opabex3d  8006  opabex3rd  8007  opabex3  8008  fparlem1  8153  fparlem2  8154  oarec  8618  ecid  8840  qsid  8841  mapval2  8930  ixpin  8981  onfin2  9294  unfilem1  9371  unifpw  9425  dfom5  9719  alephsuc2  10149  ackbij2  10311  isf33lem  10435  dffin7-2  10467  fin1a2lem6  10474  acncc  10509  fin41  10513  iunfo  10608  grutsk  10891  grothac  10899  grothtsk  10904  dfz2  12658  qexALT  13029  dfrp2  13456  om2uzrani  14003  hashkf  14381  divalglem4  16444  1nprm  16726  nsgacs  19202  oppgsubm  19405  oppgsubg  19406  oppgcntz  19407  pmtrprfvalrn  19530  opprsubg  20378  opprunit  20403  opprirred  20448  opprsubrng  20585  opprsubrg  20621  00lss  20962  dfprm2  21507  unocv  21721  iunocv  21722  00ply1bas  22262  toprntopon  22952  unisngl  23556  zcld  24854  iundisj  25602  plyun0  26256  aannenlem2  26389  eqid1  30499  choc0  31358  chocnul  31360  spanunsni  31611  lncnbd  32070  adjbd1o  32117  rnbra  32139  pjimai  32208  iunin1f  32580  iundisjf  32611  xrdifh  32785  iundisjfi  32801  opprnsg  33477  ccfldextdgrr  33682  cmpcref  33796  eulerpartgbij  34337  eulerpartlemr  34339  oddprm2  34632  dfdm5  35736  dfrn5  35737  dffix2  35869  fixcnv  35872  dfom5b  35876  fnimage  35893  brimg  35901  bj-csbsnlem  36869  bj-projun  36960  bj-pw0ALT  37015  bj-vjust  37021  finxp1o  37358  iundif1  37554  poimirlem26  37606  csbcom2fi  38088  prtlem16  38825  sn-iotalem  42214  aaitgo  43119  imaiun1  43613  grumnueq  44256  nzss  44286  dfodd2  47510  dfeven5  47540  dfodd7  47541