Theorem eqriv 2729

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  eqid  2732  cbvabv  2805  cbvabw  2806  cbvabwOLD  2807  cbvab  2808  vjust  3475  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  7240  unon  7815  opabex3d  7948  opabex3rd  7949  opabex3  7950  fparlem1  8094  fparlem2  8095  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  19223  oppgsubg  19224  oppgcntz  19225  pmtrprfvalrn  19350  opprsubg  20158  opprunit  20183  opprirred  20228  opprsubrg  20376  00lss  20544  dfprm2  21034  unocv  21224  iunocv  21225  00ply1bas  21753  toprntopon  22418  unisngl  23022  zcld  24320  iundisj  25056  plyun0  25702  aannenlem2  25833  eqid1  29709  choc0  30566  chocnul  30568  spanunsni  30819  lncnbd  31278  adjbd1o  31325  rnbra  31347  pjimai  31416  iunin1f  31776  iundisjf  31807  xrdifh  31978  iundisjfi  31994  opprnsg  32586  ccfldextdgrr  32734  cmpcref  32818  eulerpartgbij  33359  eulerpartlemr  33361  oddprm2  33655  dfdm5  34732  dfrn5  34733  dffix2  34865  fixcnv  34868  dfom5b  34872  fnimage  34889  brimg  34897  bj-csbsnlem  35771  bj-projun  35863  bj-pw0ALT  35918  bj-vjust  35924  finxp1o  36261  iundif1  36450  poimirlem26  36502  csbcom2fi  36984  prtlem16  37727  sn-iotalem  41034  aaitgo  41889  imaiun1  42387  grumnueq  43031  nzss  43061  dfodd2  46290  dfeven5  46320  dfodd7  46321  opprsubrng  46722