Theorem eqriv 2736

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  eqid  2739  cbvabv  2812  cbvabw  2813  cbvabwOLD  2814  cbvab  2815  vjust  3434  rabtru  3622  nfccdeq  3714  csbgfi  3854  difeqri  4060  uneqri  4086  ineqri  4139  symdifass  4186  indifdi  4218  indifdirOLD  4220  undif3  4225  csbcom  4352  csbab  4372  dfopif  4801  pwpr  4834  pwtp  4835  pwv  4837  uniun  4865  int0  4894  intun  4912  intprOLD  4915  iuncom  4932  iuncom4  4933  iunin2  5001  iinun2  5003  iundif2  5004  iunun  5023  iunxun  5024  iunxiun  5027  iinpw  5036  inuni  5268  unipw  5367  xpiundi  5658  xpiundir  5659  iunxpf  5760  cnvuni  5798  dmiun  5825  dmuni  5826  idinxpres  5957  rniun  6056  xpdifid  6076  cnvresima  6138  imaco  6159  rnco  6160  dfmpt3  6576  imaiun  7127  unon  7687  opabex3d  7817  opabex3rd  7818  opabex3  7819  fparlem1  7961  fparlem2  7962  oarec  8402  ecid  8580  qsid  8581  mapval2  8669  ixpin  8720  onfin2  9023  unfilem1  9087  unifpw  9131  dfom5  9417  alephsuc2  9845  ackbij2  10008  isf33lem  10131  dffin7-2  10163  fin1a2lem6  10170  acncc  10205  fin41  10209  iunfo  10304  grutsk  10587  grothac  10595  grothtsk  10600  dfz2  12347  qexALT  12713  dfrp2  13137  om2uzrani  13681  hashkf  14055  divalglem4  16114  1nprm  16393  nsgacs  18799  oppgsubm  18978  oppgsubg  18979  oppgcntz  18980  pmtrprfvalrn  19105  opprsubg  19887  opprunit  19912  opprirred  19953  opprsubrg  20054  00lss  20212  dfprm2  20704  unocv  20894  iunocv  20895  00ply1bas  21420  toprntopon  22083  unisngl  22687  zcld  23985  iundisj  24721  plyun0  25367  aannenlem2  25498  eqid1  28840  choc0  29697  chocnul  29699  spanunsni  29950  lncnbd  30409  adjbd1o  30456  rnbra  30478  pjimai  30547  iunin1f  30906  iundisjf  30937  xrdifh  31110  iundisjfi  31126  ccfldextdgrr  31751  cmpcref  31809  eulerpartgbij  32348  eulerpartlemr  32350  oddprm2  32644  dfdm5  33756  dfrn5  33757  imaindm  33762  dffix2  34216  fixcnv  34219  dfom5b  34223  fnimage  34240  brimg  34248  bj-csbsnlem  35097  bj-projun  35193  bj-pw0ALT  35231  bj-vjust  35235  finxp1o  35572  iundif1  35760  poimirlem26  35812  csbcom2fi  36295  prtlem16  36890  sn-iotalem  40196  aaitgo  40994  imaiun1  41266  grumnueq  41912  nzss  41942  dfodd2  45099  dfeven5  45129  dfodd7  45130