Theorem eqriv 2760

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqid  2763  cbvabv  2833  cbvabw  2834  cbvab  2835  vjust  3456  rabtru  3649  nfccdeq  3742  csbgfi  3874  difeqri  4084  uneqri  4111  ineqri  4166  symdifass  4216  indifdi  4248  undif3  4254  csbcom  4386  csbab  4406  pwpr  4867  pwtp  4868  pwv  4870  uniun  4896  int0  4928  intun  4946  iuncom  4965  iuncom4  4966  iunin2  5036  iinun2  5038  iundif2  5039  iunun  5060  iunxun  5061  iunxiun  5064  iinpw  5073  inuni  5322  unipw  5433  xpiundi  5734  xpiundir  5735  iunxpf  5836  cnvuni  5878  dmiun  5905  dmuni  5906  idinxpres  6051  rniun  6147  xpdifid  6167  xpdifcnvepel  6168  cnvresima  6233  imaco  6254  rnco  6255  rncoOLD  6256  imaindm  6302  dfmpt3  6671  imaiun  7245  unon  7828  opabex3d  7963  opabex3rd  7964  opabex3  7965  fparlem1  8108  fparlem2  8109  oarec  8548  ecid  8779  qsid  8780  mapval2  8871  ixpin  8922  onfin2  9202  unfilem1  9266  unifpw  9313  dfom5  9620  alephsuc2  10065  ackbij2  10226  isf33lem  10351  dffin7-2  10383  fin1a2lem6  10390  acncc  10425  fin41  10429  iunfo  10524  grutsk  10808  grothac  10816  grothtsk  10821  dfz2  12611  qexALT  12989  dfrp2  13422  om2uzrani  13990  hashkf  14370  divalglem4  16455  1nprm  16738  nsgacs  19229  oppgsubm  19433  oppgsubg  19434  oppgcntz  19435  pmtrprfvalrn  19559  opprsubg  20435  opprunit  20460  opprirred  20505  opprsubrng  20645  opprsubrg  20679  00lss  21043  dfprm2  21604  unocv  21811  iunocv  21812  00ply1bas  22380  toprntopon  23063  unisngl  23665  zcld  24952  iundisj  25688  plyun0  26335  aannenlem2  26473  dfz12s2  28662  eqid1  30799  choc0  31659  chocnul  31661  spanunsni  31912  lncnbd  32371  adjbd1o  32418  rnbra  32440  pjimai  32509  iunin1f  32883  iundisjf  32915  xrdifh  33106  iundisjfi  33122  opprnsg  33747  0mplrim  33885  ccfldextdgrr  34043  cmpcref  34221  eulerpartgbij  34743  eulerpartlemr  34745  oddprm2  35023  dfdm5  36246  dfrn5  36247  dffix2  36376  fixcnv  36379  dfom5b  36383  fnimage  36400  brimg  36408  bj-csbsnlem  37519  bj-projun  37611  bj-pw0ALT  37666  bj-vjust  37672  finxp1o  38019  iundif1  38226  poimirlem26  38278  csbcom2fi  38758  dfsucmap3  39093  prtlem16  39624  sn-iotalem  42973  redvmptabs  43102  aaitgo  43872  imaiun1  44360  grumnueq  44980  nzss  45010  dfodd2  48384  dfeven5  48414  dfodd7  48415  dfidom2  49091  ixpv  49651  isoval2  49796  oppcciceq  49813  oppczeroo  49998  dfinito4  50262  lmdfval2  50416  cmdfval2  50417  initocmd  50430  termolmd  50431