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

Theorem eqriv 2453
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
StepHypRef Expression
1 dfcleq 2450 . 2
2 eqriv.1 . 2
31, 2mpgbir 1622 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818
This theorem is referenced by:  eqid  2457  cbvab  2598  cbvabOLD  2599  vjust  3110  nfccdeq  3325  difeqri  3623  uneqri  3645  incom  3690  ineqri  3691  indifdir  3753  undif3  3758  csbcom  3837  csbab  3855  pwpr  4245  pwtp  4246  pwv  4248  uniun  4268  intun  4319  intpr  4320  iuncom  4337  iuncom4  4338  iun0  4386  0iun  4387  iunin2  4394  iinun2  4396  iundif2  4397  iunun  4411  iunxun  4412  iunxiun  4413  iinpw  4419  inuni  4614  unipw  4702  xpiundi  5059  xpiundir  5060  0xp  5085  iunxpf  5156  cnvuni  5194  dmiun  5216  dmuni  5217  epini  5372  rniun  5421  xpdifid  5440  cnvresima  5501  imaco  5517  rnco  5518  dfmpt3  5708  imaiun  6157  snnex  6606  unon  6666  opabex3d  6778  opabex3  6779  fparlem1  6900  fparlem2  6901  oarec  7230  ecid  7395  qsid  7396  mapval2  7468  ixpin  7514  onfin2  7729  unfilem1  7804  unifpw  7843  dfom5  8088  alephsuc2  8482  ackbij2  8644  isf33lem  8767  dffin7-2  8799  fin1a2lem6  8806  acncc  8841  fin41  8845  iunfo  8935  grutsk  9221  grothac  9229  grothtsk  9234  dfz2  10907  qexALT  11226  om2uzrani  12063  hashkf  12407  divalglem4  14054  1nprm  14222  nsgacs  16237  oppgsubm  16397  oppgsubg  16398  oppgcntz  16399  pmtrprfvalrn  16513  opprsubg  17285  opprunit  17310  opprirred  17351  opprsubrg  17450  00lss  17588  00ply1bas  18281  dfprm2  18524  dfprm2OLD  18527  unocv  18711  iunocv  18712  unisngl  20028  zcld  21318  iundisj  21958  plyun0  22594  aannenlem2  22725  eqid1  25175  choc0  26244  chocnul  26246  spanunsni  26497  lncnbd  26957  adjbd1o  27004  rnbra  27026  pjimai  27095  iundisjf  27448  xrdifh  27591  iundisjfi  27601  cmpcref  27853  eulerpartgbij  28311  eulerpartlemr  28313  dfdm5  29206  dfrn5  29207  symdifass  29477  dffix2  29555  fixcnv  29558  dfom5b  29562  fnimage  29579  brimg  29587  iundif1  30037  csbcom2fi  30534  csbgfi  30535  prtlem16  30610  aaitgo  31111  nzss  31222  bj-vjust  34372  bj-csbsnlem  34470  bj-projun  34552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator