Theorem eqriv 2731

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

Syntax hints:   ↔ wb 206   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  eqid  2734  cbvabv  2809  cbvabw  2810  cbvab  2811  vjust  3478  rabtru  3691  nfccdeq  3786  csbgfi  3928  difeqri  4137  uneqri  4165  ineqri  4219  symdifass  4267  indifdi  4299  undif3  4305  csbcom  4425  csbab  4445  pwpr  4905  pwtp  4906  pwv  4908  uniun  4934  int0  4966  intun  4984  iuncom  5003  iuncom4  5004  iunin2  5075  iinun2  5077  iundif2  5078  iunun  5097  iunxun  5098  iunxiun  5101  iinpw  5110  inuni  5355  unipw  5460  xpiundi  5758  xpiundir  5759  iunxpf  5861  cnvuni  5899  dmiun  5926  dmuni  5927  idinxpres  6066  rniun  6169  xpdifid  6189  cnvresima  6251  imaco  6272  rnco  6273  imaindm  6320  dfmpt3  6702  imaiun  7264  unon  7850  opabex3d  7988  opabex3rd  7989  opabex3  7990  fparlem1  8135  fparlem2  8136  oarec  8598  ecid  8820  qsid  8821  mapval2  8910  ixpin  8961  onfin2  9265  unfilem1  9340  unifpw  9392  dfom5  9687  alephsuc2  10117  ackbij2  10279  isf33lem  10403  dffin7-2  10435  fin1a2lem6  10442  acncc  10477  fin41  10481  iunfo  10576  grutsk  10859  grothac  10867  grothtsk  10872  dfz2  12629  qexALT  13003  dfrp2  13432  om2uzrani  13989  hashkf  14367  divalglem4  16429  1nprm  16712  nsgacs  19192  oppgsubm  19395  oppgsubg  19396  oppgcntz  19397  pmtrprfvalrn  19520  opprsubg  20368  opprunit  20393  opprirred  20438  opprsubrng  20575  opprsubrg  20609  00lss  20956  dfprm2  21501  unocv  21715  iunocv  21716  00ply1bas  22256  toprntopon  22946  unisngl  23550  zcld  24848  iundisj  25596  plyun0  26250  aannenlem2  26385  eqid1  30495  choc0  31354  chocnul  31356  spanunsni  31607  lncnbd  32066  adjbd1o  32113  rnbra  32135  pjimai  32204  iunin1f  32577  iundisjf  32608  xrdifh  32788  iundisjfi  32803  opprnsg  33491  ccfldextdgrr  33696  cmpcref  33810  eulerpartgbij  34353  eulerpartlemr  34355  oddprm2  34648  dfdm5  35753  dfrn5  35754  dffix2  35886  fixcnv  35889  dfom5b  35893  fnimage  35910  brimg  35918  bj-csbsnlem  36885  bj-projun  36976  bj-pw0ALT  37031  bj-vjust  37037  finxp1o  37374  iundif1  37580  poimirlem26  37632  csbcom2fi  38114  prtlem16  38850  sn-iotalem  42238  redvmptabs  42368  aaitgo  43150  imaiun1  43640  grumnueq  44282  nzss  44312  dfodd2  47560  dfeven5  47590  dfodd7  47591