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

Theorem eqriv 2082
Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-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 2079 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1385 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 103    = wceq 1287    e. wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1381  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqid  2085  sb8ab  2206  cbvab  2207  vjust  2616  nfccdeq  2827  difeqri  3109  uneqri  3131  incom  3181  ineqri  3182  difin  3225  invdif  3230  indif  3231  difundi  3240  indifdir  3244  pwv  3635  uniun  3655  intun  3702  intpr  3703  iuncom  3719  iuncom4  3720  iun0  3769  0iun  3770  iunin2  3776  iunun  3790  iunxun  3791  iunxiun  3792  iinpw  3798  inuni  3966  unidif0  3977  unipw  4018  snnex  4245  unon  4301  xpiundi  4464  xpiundir  4465  0xp  4486  iunxpf  4552  cnvuni  4590  dmiun  4613  dmuni  4614  epini  4770  rniun  4808  cnvresima  4886  imaco  4902  rnco  4903  dfmpt3  5101  imaiun  5500  opabex3d  5849  opabex3  5850  ecid  6307  qsid  6309  mapval2  6387  dfz2  8752  infssuzex  10820  1nprm  10971
  Copyright terms: Public domain W3C validator