Theorem eqriv 2733

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  eqid  2736  cbvabv  2806  cbvabw  2807  cbvab  2808  vjust  3430  rabtru  3632  nfccdeq  3724  csbgfi  3857  difeqri  4068  uneqri  4096  ineqri  4152  symdifass  4202  indifdi  4234  undif3  4240  csbcom  4360  csbab  4380  pwpr  4844  pwtp  4845  pwv  4847  uniun  4873  int0  4904  intun  4922  iuncom  4941  iuncom4  4942  iunin2  5013  iinun2  5015  iundif2  5016  iunun  5035  iunxun  5036  iunxiun  5039  iinpw  5048  inuni  5291  unipw  5402  xpiundi  5702  xpiundir  5703  iunxpf  5803  cnvuni  5841  dmiun  5868  dmuni  5869  idinxpres  6012  rniun  6111  xpdifid  6132  cnvresima  6194  imaco  6215  rnco  6216  rncoOLD  6217  imaindm  6263  dfmpt3  6632  imaiun  7200  unon  7782  opabex3d  7918  opabex3rd  7919  opabex3  7920  fparlem1  8062  fparlem2  8063  oarec  8497  ecid  8727  qsid  8728  mapval2  8820  ixpin  8871  onfin2  9151  unfilem1  9215  unifpw  9265  dfom5  9571  alephsuc2  10002  ackbij2  10164  isf33lem  10288  dffin7-2  10320  fin1a2lem6  10327  acncc  10362  fin41  10366  iunfo  10461  grutsk  10745  grothac  10753  grothtsk  10758  dfz2  12543  qexALT  12914  dfrp2  13347  om2uzrani  13914  hashkf  14294  divalglem4  16365  1nprm  16648  nsgacs  19137  oppgsubm  19337  oppgsubg  19338  oppgcntz  19339  pmtrprfvalrn  19463  opprsubg  20332  opprunit  20357  opprirred  20402  opprsubrng  20536  opprsubrg  20570  00lss  20936  dfprm2  21453  unocv  21660  iunocv  21661  00ply1bas  22203  toprntopon  22890  unisngl  23492  zcld  24779  iundisj  25515  plyun0  26162  aannenlem2  26295  dfz12s2  28480  eqid1  30537  choc0  31397  chocnul  31399  spanunsni  31650  lncnbd  32109  adjbd1o  32156  rnbra  32178  pjimai  32247  iunin1f  32627  iundisjf  32659  xrdifh  32853  iundisjfi  32869  opprnsg  33544  ccfldextdgrr  33816  cmpcref  33994  eulerpartgbij  34516  eulerpartlemr  34518  oddprm2  34799  dfdm5  35955  dfrn5  35956  dffix2  36085  fixcnv  36088  dfom5b  36092  fnimage  36109  brimg  36117  bj-csbsnlem  37210  bj-projun  37301  bj-pw0ALT  37356  bj-vjust  37362  finxp1o  37708  iundif1  37915  poimirlem26  37967  csbcom2fi  38449  dfsucmap3  38784  prtlem16  39315  sn-iotalem  42662  redvmptabs  42792  aaitgo  43590  imaiun1  44078  grumnueq  44714  nzss  44744  dfodd2  48112  dfeven5  48142  dfodd7  48143  ixpv  49365  isoval2  49510  oppcciceq  49527  oppczeroo  49712  dfinito4  49976  lmdfval2  50130  cmdfval2  50131  initocmd  50144  termolmd  50145