ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqriv Structured version   Unicode version

Theorem eqriv 2015
Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqriv.1
Assertion
Ref Expression
eqriv
Distinct variable groups:   ,   ,

Proof of Theorem eqriv
StepHypRef Expression
1 dfcleq 2012 . 2
2 eqriv.1 . 2
31, 2mpgbir 1318 1
Colors of variables: wff set class
Syntax hints:   wb 98   wceq 1226   wcel 1370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1314  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011
This theorem is referenced by:  eqid  2018  sb8ab  2137  cbvab  2138  vjust  2532  nfccdeq  2735  difeqri  3037  uneqri  3058  incom  3102  ineqri  3103  difin  3147  invdif  3152  indif  3153  difundi  3162  indifdir  3166  pwv  3549  uniun  3569  intun  3616  intpr  3617  iuncom  3633  iuncom4  3634  iun0  3683  0iun  3684  iunin2  3690  iunun  3704  iunxun  3705  iunxiun  3706  iinpw  3712  inuni  3879  unidif0  3890  unipw  3923  snnex  4127  unon  4182  xpiundi  4321  xpiundir  4322  0xp  4343  iunxpf  4407  cnvuni  4444  dmiun  4467  dmuni  4468  epini  4619  rniun  4657  cnvresima  4733  imaco  4749  rnco  4750  dfmpt3  4943  imaiun  5320  opabex3d  5667  opabex3  5668  ecid  6076  qsid  6078
  Copyright terms: Public domain W3C validator