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

Theorem eqriv 2154
 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 2151 . 2
2 eqriv.1 . 2
31, 2mpgbir 1433 1
 Colors of variables: wff set class Syntax hints:   wb 104   wceq 1335   wcel 2128 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1429  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-cleq 2150 This theorem is referenced by:  eqid  2157  sb8ab  2279  cbvabw  2280  cbvab  2281  vjust  2713  nfccdeq  2935  csbcow  3042  difeqri  3227  uneqri  3249  incom  3299  ineqri  3300  difin  3344  invdif  3349  indif  3350  difundi  3359  indifdir  3363  pwv  3771  uniun  3791  intun  3838  intpr  3839  iuncom  3855  iuncom4  3856  iun0  3905  0iun  3906  iunin2  3912  iunun  3927  iunxun  3928  iunxiun  3930  iinpw  3939  inuni  4116  unidif0  4127  unipw  4176  snnex  4406  unon  4468  xpiundi  4641  xpiundir  4642  0xp  4663  iunxpf  4731  cnvuni  4769  dmiun  4792  dmuni  4793  epini  4954  rniun  4993  cnvresima  5072  imaco  5088  rnco  5089  dfmpt3  5289  imaiun  5705  opabex3d  6063  opabex3  6064  ecid  6536  qsid  6538  mapval2  6616  ixpin  6661  dfz2  9219  dfrp2  10145  infssuzex  11817  1nprm  11971
 Copyright terms: Public domain W3C validator