Theorem eqriv 2732

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  eqid  2735  cbvabv  2805  cbvabw  2806  cbvab  2807  vjust  3460  rabtru  3668  nfccdeq  3761  csbgfi  3894  difeqri  4103  uneqri  4131  ineqri  4187  symdifass  4237  indifdi  4269  undif3  4275  csbcom  4395  csbab  4415  pwpr  4877  pwtp  4878  pwv  4880  uniun  4906  int0  4938  intun  4956  iuncom  4975  iuncom4  4976  iunin2  5047  iinun2  5049  iundif2  5050  iunun  5069  iunxun  5070  iunxiun  5073  iinpw  5082  inuni  5320  unipw  5425  xpiundi  5725  xpiundir  5726  iunxpf  5828  cnvuni  5866  dmiun  5893  dmuni  5894  idinxpres  6034  rniun  6136  xpdifid  6157  cnvresima  6219  imaco  6240  rnco  6241  imaindm  6288  dfmpt3  6672  imaiun  7237  unon  7825  opabex3d  7964  opabex3rd  7965  opabex3  7966  fparlem1  8111  fparlem2  8112  oarec  8574  ecid  8796  qsid  8797  mapval2  8886  ixpin  8937  onfin2  9240  unfilem1  9315  unifpw  9367  dfom5  9664  alephsuc2  10094  ackbij2  10256  isf33lem  10380  dffin7-2  10412  fin1a2lem6  10419  acncc  10454  fin41  10458  iunfo  10553  grutsk  10836  grothac  10844  grothtsk  10849  dfz2  12607  qexALT  12980  dfrp2  13411  om2uzrani  13970  hashkf  14350  divalglem4  16415  1nprm  16698  nsgacs  19145  oppgsubm  19345  oppgsubg  19346  oppgcntz  19347  pmtrprfvalrn  19469  opprsubg  20312  opprunit  20337  opprirred  20382  opprsubrng  20519  opprsubrg  20553  00lss  20898  dfprm2  21434  unocv  21640  iunocv  21641  00ply1bas  22175  toprntopon  22863  unisngl  23465  zcld  24753  iundisj  25501  plyun0  26154  aannenlem2  26289  eqid1  30448  choc0  31307  chocnul  31309  spanunsni  31560  lncnbd  32019  adjbd1o  32066  rnbra  32088  pjimai  32157  iunin1f  32538  iundisjf  32570  xrdifh  32757  iundisjfi  32773  opprnsg  33499  ccfldextdgrr  33713  cmpcref  33881  eulerpartgbij  34404  eulerpartlemr  34406  oddprm2  34687  dfdm5  35790  dfrn5  35791  dffix2  35923  fixcnv  35926  dfom5b  35930  fnimage  35947  brimg  35955  bj-csbsnlem  36921  bj-projun  37012  bj-pw0ALT  37067  bj-vjust  37073  finxp1o  37410  iundif1  37618  poimirlem26  37670  csbcom2fi  38152  prtlem16  38887  sn-iotalem  42272  redvmptabs  42403  aaitgo  43186  imaiun1  43675  grumnueq  44311  nzss  44341  dfodd2  47650  dfeven5  47680  dfodd7  47681  ixpv  48865  oppcciceq  49019  oppczeroo  49154  dfinito4  49386  lmdfval2  49527  cmdfval2  49528