Theorem eqriv 2755

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

Syntax hints:   ↔ wb 209   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750

This theorem is referenced by:  eqid  2758  cbvabv  2826  cbvabw  2827  cbvabwOLD  2828  cbvab  2829  vjust  3410  rabtru  3601  nfccdeq  3694  csbgfi  3827  difeqri  4032  uneqri  4058  incomOLD  4109  ineqri  4110  symdifass  4158  indifdi  4190  indifdirOLD  4192  undif3  4197  csbcom  4317  csbab  4337  dfopif  4760  pwpr  4795  pwtp  4796  pwv  4798  uniun  4826  int0  4855  intun  4873  intprOLD  4876  iuncom  4893  iuncom4  4894  iunin2  4962  iinun2  4964  iundif2  4965  iunun  4984  iunxun  4985  iunxiun  4988  iinpw  4997  inuni  5217  unipw  5315  xpiundi  5596  xpiundir  5597  iunxpf  5694  cnvuni  5732  dmiun  5759  dmuni  5760  idinxpres  5891  epini  5936  rniun  5983  xpdifid  6002  cnvresima  6064  imaco  6086  rnco  6087  dfmpt3  6470  imaiun  7002  unon  7551  opabex3d  7676  opabex3rd  7677  opabex3  7678  fparlem1  7818  fparlem2  7819  oarec  8204  ecid  8378  qsid  8379  mapval2  8467  ixpin  8518  onfin2  8762  unfilem1  8828  unifpw  8873  dfom5  9159  alephsuc2  9553  ackbij2  9716  isf33lem  9839  dffin7-2  9871  fin1a2lem6  9878  acncc  9913  fin41  9917  iunfo  10012  grutsk  10295  grothac  10303  grothtsk  10308  dfz2  12052  qexALT  12417  dfrp2  12841  om2uzrani  13382  hashkf  13755  divalglem4  15810  1nprm  16089  nsgacs  18395  oppgsubm  18571  oppgsubg  18572  oppgcntz  18573  pmtrprfvalrn  18697  opprsubg  19471  opprunit  19496  opprirred  19537  opprsubrg  19638  00lss  19795  dfprm2  20277  unocv  20459  iunocv  20460  00ply1bas  20978  toprntopon  21639  unisngl  22241  zcld  23528  iundisj  24262  plyun0  24907  aannenlem2  25038  eqid1  28365  choc0  29222  chocnul  29224  spanunsni  29475  lncnbd  29934  adjbd1o  29981  rnbra  30003  pjimai  30072  iunin1f  30433  iundisjf  30464  xrdifh  30638  iundisjfi  30654  ccfldextdgrr  31276  cmpcref  31334  eulerpartgbij  31871  eulerpartlemr  31873  oddprm2  32167  dfdm5  33276  dfrn5  33277  imaindm  33282  dffix2  33791  fixcnv  33794  dfom5b  33798  fnimage  33815  brimg  33823  bj-csbsnlem  34659  bj-projun  34746  bj-pw0ALT  34783  bj-vjust  34787  finxp1o  35124  wl-dfrabv  35342  iundif1  35346  poimirlem26  35398  csbcom2fi  35881  prtlem16  36480  aaitgo  40524  imaiun1  40770  grumnueq  41413  nzss  41439  dfodd2  44580  dfeven5  44610  dfodd7  44611