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

Theorem eqriv 2440
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 2437 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1595 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-cleq 2436
This theorem is referenced by:  eqid  2443  cbvab  2561  vjust  2973  nfccdeq  3184  difeqri  3476  uneqri  3498  incom  3543  ineqri  3544  indifdir  3606  undif3  3611  csbcom  3689  csbab  3707  pwpr  4087  pwtp  4088  pwv  4090  uniun  4110  intun  4160  intpr  4161  iuncom  4177  iuncom4  4178  iun0  4226  0iun  4227  iunin2  4234  iinun2  4236  iundif2  4237  iunun  4251  iunxun  4252  iunxiun  4253  iinpw  4259  inuni  4454  unipw  4542  xpiundi  4893  xpiundir  4894  0xp  4917  iunxpf  4988  cnvuni  5026  dmiun  5048  dmuni  5049  epini  5199  rniun  5247  xpdifid  5266  cnvresima  5327  imaco  5343  rnco  5344  dfmpt3  5533  imaiun  5962  snnex  6382  unon  6442  opabex3d  6555  opabex3  6556  fparlem1  6672  fparlem2  6673  oarec  7001  ecid  7165  qsid  7166  mapval2  7242  ixpin  7288  onfin2  7502  unfilem1  7576  unifpw  7614  dfom5  7856  alephsuc2  8250  ackbij2  8412  isf33lem  8535  dffin7-2  8567  fin1a2lem6  8574  acncc  8609  fin41  8613  iunfo  8703  grutsk  8989  grothac  8997  grothtsk  9002  dfz2  10664  qexALT  10968  om2uzrani  11775  hashkf  12105  divalglem4  13600  1nprm  13768  nsgacs  15717  oppgsubm  15877  oppgsubg  15878  oppgcntz  15879  pmtrprfvalrn  15994  opprsubg  16728  opprunit  16753  opprirred  16794  opprsubrg  16886  00lss  17023  00ply1bas  17695  dfprm2  17918  dfprm2OLD  17921  unocv  18105  iunocv  18106  zcld  20390  iundisj  21029  plyun0  21665  aannenlem2  21795  eqid1  23660  choc0  24729  chocnul  24731  spanunsni  24982  lncnbd  25442  adjbd1o  25489  rnbra  25511  pjimai  25580  iundisjf  25931  xrdifh  26070  iundisjfi  26080  eulerpartgbij  26755  eulerpartlemr  26757  dfdm5  27587  dfrn5  27588  symdifass  27858  dffix2  27936  fixcnv  27939  dfom5b  27943  fnimage  27960  brimg  27968  iundif1  28413  csbcom2fi  28938  csbgfi  28939  prtlem16  29014  aaitgo  29519  bj-vjust  32307  bj-csbsnlem  32405  bj-projun  32487
  Copyright terms: Public domain W3C validator