MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqriv Structured version   Visualization version   Unicode version

Theorem eqriv 2468
Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
eqriv.1  |-  ( x  e.  A  <->  x  e.  B )
Assertion
Ref Expression
eqriv  |-  A  =  B
Distinct variable groups:    x, A    x, B

Proof of Theorem eqriv
StepHypRef Expression
1 dfcleq 2465 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1681 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    = wceq 1452    e. wcel 1904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-cleq 2464
This theorem is referenced by:  eqid  2471  cbvab  2594  vjust  3032  nfccdeq  3253  difeqri  3542  uneqri  3567  incom  3616  ineqri  3617  symdifass  3663  indifdir  3690  undif3  3695  csbcom  3787  csbab  3801  pwpr  4186  pwtp  4187  pwv  4189  uniun  4209  intun  4258  intpr  4259  iuncom  4276  iuncom4  4277  iun0  4325  0iun  4326  iunin2  4333  iinun2  4335  iundif2  4336  iunun  4353  iunxun  4354  iunxiun  4357  iinpw  4363  inuni  4563  unipw  4650  xpiundi  4894  xpiundir  4895  0xp  4920  iunxpf  4988  cnvuni  5026  dmiun  5049  dmuni  5050  epini  5204  rniun  5252  xpdifid  5271  cnvresima  5331  imaco  5347  rnco  5348  dfmpt3  5708  imaiun  6168  snnex  6616  unon  6677  opabex3d  6790  opabex3  6791  fparlem1  6915  fparlem2  6916  oarec  7281  ecid  7446  qsid  7447  mapval2  7519  ixpin  7565  onfin2  7782  unfilem1  7853  unifpw  7895  dfom5  8173  alephsuc2  8529  ackbij2  8691  isf33lem  8814  dffin7-2  8846  fin1a2lem6  8853  acncc  8888  fin41  8892  iunfo  8982  grutsk  9265  grothac  9273  grothtsk  9278  dfz2  10979  qexALT  11302  om2uzrani  12204  hashkf  12555  divalglem4  14454  1nprm  14708  nsgacs  16931  oppgsubm  17091  oppgsubg  17092  oppgcntz  17093  pmtrprfvalrn  17207  opprsubg  17942  opprunit  17967  opprirred  18008  opprsubrg  18107  00lss  18243  00ply1bas  18910  dfprm2  19142  unocv  19320  iunocv  19321  unisngl  20619  zcld  21909  iundisj  22580  plyun0  23230  aannenlem2  23364  eqid1  25983  choc0  27060  chocnul  27062  spanunsni  27313  lncnbd  27772  adjbd1o  27819  rnbra  27841  pjimai  27910  rabtru  28214  iunin1f  28249  iundisjf  28276  dfrp2  28427  xrdifh  28437  iundisjfi  28447  cmpcref  28751  eulerpartgbij  29278  eulerpartlemr  29280  dfdm5  30489  dfrn5  30490  dffix2  30743  fixcnv  30746  dfom5b  30750  fnimage  30767  brimg  30775  bj-vjust  31467  bj-csbsnlem  31573  bj-projun  31658  finxp0  31853  finxp1o  31854  iundif1  31991  poimirlem26  32030  csbcom2fi  32433  csbgfi  32434  prtlem16  32505  aaitgo  36099  imaiun1  36314  nzss  36736  dfodd2  38911  dfeven5  38941  dfodd7  38942
  Copyright terms: Public domain W3C validator